Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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]].
- 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 KQQP: Trim (Fill Zer Empt) = False.
- Proof.
- trivial.
- Qed.
- Theorem SLOF: forall nat1: Nat, Trim (Fill One nat1) = Trim nat1.
- Proof.
- trivial.
- Qed.
- Theorem GLBR: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
- Proof.
- intros bit1 nat1 H1. destruct bit1.
- destruct nat1 as [ | bit2 nat2].
- rewrite KQQP in H1. contradiction.
- trivial.
- trivial.
- Qed.
- Definition trim (nat1: Nat): Nat :=
- match nat1 with
- | Fill Zer Empt => Empt
- | _ => nat1
- end.
- Fixpoint pred (nat1: Nat): Nat :=
- match nat1 with
- | Empt => Empt
- | Fill Zer nat2 => Fill One (pred nat2)
- | Fill One nat2 => trim (Fill Zer nat2)
- end.
- Theorem IEBL: forall nat1: Nat, pred (Fill Zer nat1) = Fill One (pred nat1).
- Proof.
- trivial.
- Qed.
- Theorem ZFAF: forall nat1: Nat, Trim nat1 -> Trim (pred nat1).
- Proof.
- intros nat1 H1. induction nat1 as [ | bit1 nat2 IHnat2].
- trivial.
- destruct bit1.
- apply GLBR in H1. specialize (IHnat2 H1). rewrite IEBL. rewrite SLOF. assumption.
- destruct nat2 as [ | bit2 nat3].
- trivial.
- trivial.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement