CoursePisa2014: ambient_logic_solution.ec

File ambient_logic_solution.ec, 4.1 KB (added by François Dupressoir, 3 years ago)

Solutions to first exercise sheet.

Line 
1(* type definitions *)
2
3(* Define type type of pairs over 'a && 'b *)
4(* <remove> *)
5type ('a, 'b) pair = 'a * 'b.
6(* </remove> *)
7
8(* <uncomment>
9   type ... pair = ... *)
10
11(* Definition pair projectors *)
12(* <remove> *)
13op fst ['a 'b] (x : ('a, 'b) pair) = let (x1, x2) = x in x1.
14op snd ['a 'b] (x : ('a, 'b) pair) = let (x1, x2) = x in x2.
15(* </remove> *)
16
17(* <uncomment>
18   op fst ...
19   op snd ... *)
20
21lemma pairE (x : 'a * 'b): (fst x, snd x) = x.
22proof.
23  (* <remove> *)
24  rewrite /fst /snd; elim x=> /= x1 x2; reflexivity.
25  (* </remove> *)
26qed.
27
28(* minimal logic : no smt/progress/trivial *)
29lemma pp b: b => b.
30proof.
31 (* <remove> *)
32 move=> hb; apply hb.
33 (* </remove> *)
34qed.
35
36lemma pp_pp b: (b => b) => b => b.
37proof.
38 (* <remove> *)
39 move=> hbb; apply hbb.
40 (* </remove> *)
41qed.
42
43lemma imp_trans b1 b2 b3: (b1 => b2) => (b2 => b3) => b1 => b3.
44proof.
45 (* <remove> *)
46 move=> hb12 hb23 hb1; apply hb23; apply hb12; assumption.
47 (* </remove> *)
48qed.
49
50lemma imp_perm b1 b2 b3: (b1 => b2 => b3) => b2 => b1 => b3.
51proof.
52 (* <remove> *)
53 move=> hb123 hb2 hb3; apply hb123; assumption.
54 (* </remove> *)
55qed.
56
57lemma imp_weak b1 b2 b3: (b1 => b3) => b1 => b2 => b3.
58proof.
59 (* <remove> *)
60 move=> hb13 hb1 _; apply hb13; assumption.
61 (* </remove> *)
62qed.
63
64lemma imp_dupL b1 b2: (b1 => b1 => b2) => b1 => b2.
65proof.
66 (* <remove> *)
67 move=> hb112 hb1; apply hb112; assumption.
68 (* </remove> *)
69qed.
70
71lemma delta_dupR b1 b2: (b1 => b2) => b1 => b1 => b2.
72proof.
73  (* <remove> *)
74  move=> hb12 _; apply hb12.
75  (* </remove> *)
76qed.
77
78lemma diamond b1 b2 b3 b4:
79  (b1 => b2) => (b1 => b3) => (b2 => b3 => b4) => b1 => b4.
80proof.
81  (* <remove> *)
82  move=> hb12 hb13 hb234 hb1; apply hb234.
83  (**) apply hb12; assumption.
84  (**) apply hb13; assumption.
85  (* </remove> *)
86qed.
87
88lemma weak_peirce b1 b2: ((((b1 => b2) => b1) => b1) => b2) => b2.
89proof.
90  (* <remove> *)
91  move=> h; apply h => h'; apply h' => hb1.
92  apply h=> _; assumption.
93  (* </remove> *)
94qed.
95
96type t.
97
98lemma LQ (p1 p2 q : t -> bool) x:
99  ((forall y, q y => p1 y /\ p2 y) /\ q x) => p1 x /\ p2 x.
100proof.
101  (* <remove> *)
102  move=> [h hq]; split; elim (h x _).
103    assumption.
104    move=> p1_x _; assumption.
105    assumption.
106    move=> _ p2_x; assumption.
107  (* </remove> *)
108qed.
109
110(* induction *)
111require import Int.
112
113print axiom Int.Induction.strongInduction.
114
115(* lemma strongInduction  (p : int -> bool):
116 *  (forall (j : int),
117 *     0 <= j => (forall (k : int), 0 <= k => k < j => p k) => p j) =>
118 *  forall (i : int), 0 <= i => p i.
119 *)
120
121(* You can use [smt] for arithmetic tautologies *)
122lemma int_ind2 (p : int -> bool):
123  p 0 => p 1 => (forall i, 0 <= i => p i => p (i+1) => p (i+2)) =>
124    forall i, 0 <= i => p i.
125proof.
126  (* <remove> *)
127  move=> p0 p1 pS2 i; elim/Int.Induction.strongInduction i.
128  move=> j ge0_j h.
129    case (j = 0); first by move=> ->; assumption.
130    case (j = 1); first by move=> ->; assumption.
131  move=> eq1_j eq0_j; rewrite (_ : j = j - 2 + 2); first by smt.
132  by apply pS2; smt.
133  (* </remove> *)
134qed. 
135
136(* definition the even/odd predicates *)
137
138pred even (n : int) = exists p, n = 2 * p.
139pred odd  (n : int) = exists p, n = 2 * p + 1.
140
141op evenA : int -> bool.
142op  oddA : int -> bool.
143
144axiom evenA0: evenA 0.
145
146axiom evenAS: forall (n : int), 0 <= n => evenA n =>  oddA (n+1).
147axiom  oddAS: forall (n : int), 0 <= n =>  oddA n => evenA (n+1).
148
149lemma oddA1: oddA 1.
150proof.
151  (* <remove> *)
152  by apply (evenAS 0 _ _) => //; apply evenA0.
153  (* </remove> *)
154qed.
155
156lemma evenAS2 (n : int): 0 <= n => evenA n => evenA (n+2).
157proof.
158  (* <remove> *)
159  move=> ge0_n evenA_n; rewrite (_ : n+2 = n+1+1); first smt.
160  apply oddAS; first smt. apply evenAS; first smt.
161  assumption.
162  (* </remove> *)
163qed.
164
165lemma oddAS2 (n : int): 0 <= n => oddA n => oddA (n+2).
166proof.
167  (* <remove> *)
168  move=> ge0_n evenA_n; rewrite (_ : n+2 = n+1+1); first smt.
169  apply evenAS; first smt. apply oddAS; first smt.
170  assumption.
171  (* </remove> *)
172qed. 
173
174lemma evenP (n : int): 0 <= n => even n => evenA n.
175proof.
176  (* <remove> *)
177  elim/int_ind2 n => //; first 2 smt.
178  move=> i ge0_i evenPi evenPSi evenSSi.
179  apply evenAS2 => //; apply evenPi; elim evenSSi=> j Ej.
180  by exists (j-1); smt.
181  (* </remove> *)
182qed.