Check out the Pastebin Gadgets Shop. We have thousands of fun, geeky & affordable gadgets on sale :-)Want more features on Pastebin? Sign Up, it's FREE!

# Untitled

By: a guest on Nov 29th, 2012  |  syntax: None  |  size: 1.47 KB  |  views: 9  |  expires: Never
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
1. Inductive Bit: Set :=
2.   | Zer: Bit
3.   | One: Bit.
4.
5. Inductive List (set1: Set): Set :=
6.   | Empt: List set1
7.   | Fill: set1 -> List set1 -> List set1.
8.
9. Implicit Arguments Empt [[set1]].
10. Implicit Arguments Fill [[set1]].
11.
12. Definition Nat: Set := List Bit.
13.
14. Fixpoint Trim (nat1: Nat): Prop :=
15.   match nat1 with
16.   | Empt => True
17.   | Fill Zer Empt => False
18.   | Fill _ nat2 => Trim nat2
19.   end.
20.
21. Theorem KQQP: Trim (Fill Zer Empt) = False.
22. Proof.
23. trivial.
24. Qed.
25.
26. Theorem SLOF: forall nat1: Nat, Trim (Fill One nat1) = Trim nat1.
27. Proof.
28. trivial.
29. Qed.
30.
31. Theorem GLBR: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
32. Proof.
33. intros bit1 nat1 H1. destruct bit1.
34.   destruct nat1 as [ | bit2 nat2].
35.     rewrite KQQP in H1. contradiction.
36.     trivial.
37.   trivial.
38. Qed.
39.
40. Definition trim (nat1: Nat): Nat :=
41.   match nat1 with
42.   | Fill Zer Empt => Empt
43.   | _ => nat1
44.   end.
45.
46. Fixpoint pred (nat1: Nat): Nat :=
47.   match nat1 with
48.   | Empt => Empt
49.   | Fill Zer nat2 => Fill One (pred nat2)
50.   | Fill One nat2 => trim (Fill Zer nat2)
51.   end.
52.
53. Theorem IEBL: forall nat1: Nat, pred (Fill Zer nat1) = Fill One (pred nat1).
54. Proof.
55. trivial.
56. Qed.
57.
58. Theorem ZFAF: forall nat1: Nat, Trim nat1 -> Trim (pred nat1).
59. Proof.
60. intros nat1 H1. induction nat1 as [ | bit1 nat2 IHnat2].
61.   trivial.
62.   destruct bit1.
63.     apply GLBR in H1. specialize (IHnat2 H1). rewrite IEBL. rewrite SLOF. assumption.
64.     destruct nat2 as [ | bit2 nat3].
65.       trivial.
66.       trivial.
67. Qed.
clone this paste RAW Paste Data
Top