Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement