• Sign Up
• Login
• API
• FAQ
• Tools
• Trends
• Archive
SHARE
TWEET

# Untitled

a guest Nov 29th, 2012 10 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
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.
RAW Paste Data
Top