Require Import Coq.Program.Program.
Inductive Bit: Set :=
| Zer: Bit
| One: Bit.
Inductive List (set1: Set): Set :=
| Empt: List set1
| Fill: set1 -> List set1 -> List set1.
Implicit Arguments Empt [[set1]].
Implicit Arguments Fill [[set1]].
Fixpoint meas {set1: Set} (list1: List set1): nat :=
match list1 with
| Empt => O
| Fill _ list2 => S (meas list2)
end.
Definition Nat: Set := List Bit.
Fixpoint Trim (nat1: Nat): Prop :=
match nat1 with
| Empt => True
| Fill Zer Empt => False
| Fill _ nat2 => Trim nat2
end.
Theorem VEGC: Trim (Fill Zer Empt) = False.
Proof.
trivial.
Qed.
Theorem MCOW: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
Proof.
destruct bit1.
destruct nat1 as [ | bit2 nat2].
intro H1. rewrite VEGC in H1. contradiction.
trivial.
trivial.
Qed.
Fixpoint Pos (nat1: Nat): Prop :=
match nat1 with
| Empt => False
| Fill Zer nat2 => Pos nat2
| Fill One _ => True
end.
Theorem NXJN: Pos Empt = False.
Proof.
trivial.
Qed.
Theorem ZJSN: forall nat1: Nat, Pos (Fill Zer nat1) = Pos nat1.
Proof.
trivial.
Qed.
Definition trim (nat1: Nat): Nat :=
match nat1 with
| Fill Zer Empt => Empt
| _ => nat1
end.
Program Fixpoint pred (nat1: Nat | Trim nat1 /\ Pos nat1) {measure (meas nat1)}: Nat :=
match nat1 with
| Empt => _
| Fill Zer nat3 => Fill One (pred nat3)
| Fill One nat3 => trim (Fill Zer nat3)
end.
Next Obligation.
rewrite NXJN in p. contradiction.
Qed.
Next Obligation.
apply MCOW in t. rewrite ZJSN in p. split.
assumption.
assumption.
Qed.
Theorem ZJBJ: forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1).
Proof.
destruct nat1 as [nat3 H1]. decompose [and] H1. induction nat3 as [ | bit1 nat4].
rewrite NXJN in H0. contradiction.
destruct bit1.