CoursePisa2014: ambient_logic_clean.ec

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

Exercise Sheet day 1

Line 
1(* type definitions *)
2
3(* Define type type of pairs over 'a && 'b *)
4(* FILL ME *)
5
6type ... pair = ...
7
8
9(* Definition pair projectors *)
10(* FILL ME *)
11
12op fst ...
13op snd ...
14
15
16lemma pairE (x : 'a * 'b): (fst x, snd x) = x.
17proof.
18(* FILL ME *)
19qed.
20
21(* minimal logic : no smt/progress/trivial *)
22lemma pp b: b => b.
23proof.
24(* FILL ME *)
25qed.
26
27lemma pp_pp b: (b => b) => b => b.
28proof.
29(* FILL ME *)
30qed.
31
32lemma imp_trans b1 b2 b3: (b1 => b2) => (b2 => b3) => b1 => b3.
33proof.
34(* FILL ME *)
35qed.
36
37lemma imp_perm b1 b2 b3: (b1 => b2 => b3) => b2 => b1 => b3.
38proof.
39(* FILL ME *)
40qed.
41
42lemma imp_weak b1 b2 b3: (b1 => b3) => b1 => b2 => b3.
43proof.
44(* FILL ME *)
45qed.
46
47lemma imp_dupL b1 b2: (b1 => b1 => b2) => b1 => b2.
48proof.
49(* FILL ME *)
50qed.
51
52lemma delta_dupR b1 b2: (b1 => b2) => b1 => b1 => b2.
53proof.
54(* FILL ME *)
55qed.
56
57lemma diamond b1 b2 b3 b4:
58  (b1 => b2) => (b1 => b3) => (b2 => b3 => b4) => b1 => b4.
59proof.
60(* FILL ME *)
61qed.
62
63lemma weak_peirce b1 b2: ((((b1 => b2) => b1) => b1) => b2) => b2.
64proof.
65(* FILL ME *)
66qed.
67
68type t.
69
70lemma LQ (p1 p2 q : t -> bool) x:
71  ((forall y, q y => p1 y /\ p2 y) /\ q x) => p1 x /\ p2 x.
72proof.
73(* FILL ME *)
74qed.
75
76(* induction *)
77require import Int.
78
79print axiom Int.Induction.strongInduction.
80
81(* lemma strongInduction  (p : int -> bool):
82 *  (forall (j : int),
83 *     0 <= j => (forall (k : int), 0 <= k => k < j => p k) => p j) =>
84 *  forall (i : int), 0 <= i => p i.
85 *)
86
87(* You can use [smt] for arithmetic tautologies *)
88lemma int_ind2 (p : int -> bool):
89  p 0 => p 1 => (forall i, 0 <= i => p i => p (i+1) => p (i+2)) =>
90    forall i, 0 <= i => p i.
91proof.
92(* FILL ME *)
93qed. 
94
95(* definition the even/odd predicates *)
96
97pred even (n : int) = exists p, n = 2 * p.
98pred odd  (n : int) = exists p, n = 2 * p + 1.
99
100op evenA : int -> bool.
101op  oddA : int -> bool.
102
103axiom evenA0: evenA 0.
104
105axiom evenAS: forall (n : int), 0 <= n => evenA n =>  oddA (n+1).
106axiom  oddAS: forall (n : int), 0 <= n =>  oddA n => evenA (n+1).
107
108lemma oddA1: oddA 1.
109proof.
110(* FILL ME *)
111qed.
112
113lemma evenAS2 (n : int): 0 <= n => evenA n => evenA (n+2).
114proof.
115(* FILL ME *)
116qed.
117
118lemma oddAS2 (n : int): 0 <= n => oddA n => oddA (n+2).
119proof.
120(* FILL ME *)
121qed. 
122
123lemma evenP (n : int): 0 <= n => even n => evenA n.
124proof.
125(* FILL ME *)
126qed.
127