• API
• FAQ
• Tools
• Trends
• Archive
SHARE
TWEET

# Untitled

a guest Nov 28th, 2012 15 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Require Import Coq.Program.Program.
2.
3. Inductive Bit: Set :=
4.   | Zer: Bit
5.   | One: Bit.
6.
7. Inductive List (set1: Set): Set :=
8.   | Empt: List set1
9.   | Fill: set1 -> List set1 -> List set1.
10.
11. Implicit Arguments Empt [[set1]].
12.
13. Implicit Arguments Fill [[set1]].
14.
15. Fixpoint meas {set1: Set} (list1: List set1): nat :=
16.   match list1 with
17.   | Empt => O
18.   | Fill _ list2 => S (meas list2)
19.   end.
20.
21. Definition Nat: Set := List Bit.
22.
23. Fixpoint Trim (nat1: Nat): Prop :=
24.   match nat1 with
25.   | Empt => True
26.   | Fill Zer Empt => False
27.   | Fill _ nat2 => Trim nat2
28.   end.
29.
30. Theorem VEGC: Trim (Fill Zer Empt) = False.
31. Proof.
32. trivial.
33. Qed.
34.
35. Theorem MCOW: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
36. Proof.
37. destruct bit1.
38.   destruct nat1 as [ | bit2 nat2].
39.     intro H1. rewrite VEGC in H1. contradiction.
40.     trivial.
41.   trivial.
42. Qed.
43.
44. Fixpoint Pos (nat1: Nat): Prop :=
45.   match nat1 with
46.   | Empt => False
47.   | Fill Zer nat2 => Pos nat2
48.   | Fill One _ => True
49.   end.
50.
51. Theorem NXJN: Pos Empt = False.
52. Proof.
53. trivial.
54. Qed.
55.
56. Theorem ZJSN: forall nat1: Nat, Pos (Fill Zer nat1) = Pos nat1.
57. Proof.
58. trivial.
59. Qed.
60.
61. Definition trim (nat1: Nat): Nat :=
62.   match nat1 with
63.   | Fill Zer Empt => Empt
64.   | _ => nat1
65.   end.
66.
67. Program Fixpoint pred (nat1: Nat | Trim nat1 /\ Pos nat1) {measure (meas nat1)}: Nat :=
68.   match nat1 with
69.   | Empt => _
70.   | Fill Zer nat3 => Fill One (pred nat3)
71.   | Fill One nat3 => trim (Fill Zer nat3)
72.   end.
73.
74. Next Obligation.
75. rewrite NXJN in p. contradiction.
76. Qed.
77.
78. Next Obligation.
79. apply MCOW in t. rewrite ZJSN in p. split.
80.   assumption.
81.   assumption.
82. Qed.
83.
84. Theorem ZJBJ: forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1).
85. Proof.
86. destruct nat1 as [nat3 H1]. decompose [and] H1. induction nat3 as [ | bit1 nat4].
87.   rewrite NXJN in H0. contradiction.
88.   destruct bit1.
RAW Paste Data
Top