-
Notifications
You must be signed in to change notification settings - Fork 16
/
Copy pathClase10.Tac.Automation.fst
169 lines (131 loc) · 4.58 KB
/
Clase10.Tac.Automation.fst
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
module Clase10.Tac.Automation
open FStar.Tactics
(*
As you have seen, doing constructive proofs by hand can get tedious. We
can instead write automated procedures for some classes of proofs, that
we can call over and over again when we need them, which is the main
motivation for tactic engines in other languages.
Some simple procedures are implemented in the standard library. For
instance, `assumption` tries to solve the current goal from the
hypotheses in the context. Let's first write a tactic that introduces
all implications and then calls `assumption`. (You can look at the
definition of `assumption` in FStar.Tactics.Derived.)
*)
(* Exercise: what does `l_intros` do? Look at its definition to find out. *)
let triv () : Tac unit =
let _ = l_intros () in
assumption ();
qed ()
(* Now we can call it on different goals *)
let ea1 (p q r : prop) =
assert (p ==> q ==> r ==> p)
by (triv ())
let ea2 (p q r : prop) =
assert (p ==> q ==> r ==> q)
by (triv ())
let ea3 (p q r : prop) =
assert (p ==> q ==> r ==> r)
by (triv ())
let ea4 (p q r : prop) =
assert (p ==> q ==> r ==> (forall (x:int). r))
by (triv ())
(* This simple tactic will not work with conjunctions, though. Try it! *)
//let ea5 (p q : prop) =
// assert (p ==> q ==> p /\ q)
// by (triv ())
(*
We can improve the tactic to also call `split` when the goal is a
conjunction. To do that we need a way to inspect the goal. The most
comfortable way to do that here is by calling `cur_formula ()`, which
returns the current goal represented as a value in the `formula` type.
noeq type formula =
| True_ : formula
| False_ : formula
| Comp : comparison -> term -> term -> formula
| And : term -> term -> formula
| Or : term -> term -> formula
| Not : term -> formula
| Implies: term -> term -> formula
| Iff : term -> term -> formula
| Forall : bv -> term -> formula
| Exists : bv -> term -> formula
| App : term -> term -> formula
| Name : bv -> formula
| FV : fv -> formula
| IntLit : int -> formula
| F_Unknown : formula
When `cur_formula` returns an `And`, we will call `split`, and then
recursively executing our tactic on each subgoal, with the help of
`seq`. Running `seq t1 t2` will run `t1` and then, for all new goals,
run `t2` on each, so we recurse on both conjuncts. The `split` tactic
fails (i.e. raises an exception) when the goal is not a conjunction, so
we will only do that when the goal is indeed a conjunction.
*)
let rec conjt () : Tac unit =
let _ = l_intros () in
match cur_formula () with
| And _ _ -> seq split conjt
(* otherwise, just try to solve via an assumption *)
| _ -> (assumption (); qed ())
(* Now, we can prove all of the previous formulae, plus the one with a
conjunction, and more. *)
let ea1' (p q r : prop) =
assert (p ==> q ==> r ==> p)
by (conjt ())
let ea2' (p q r : prop) =
assert (p ==> q ==> r ==> q)
by (conjt ())
let ea3' (p q r : prop) =
assert (p ==> q ==> r ==> r)
by (conjt ())
let ea4' (p q r : prop) =
assert (p ==> q ==> r ==> (forall (x:int). r))
by (conjt ())
let ea5' (p q : prop) =
assert (p ==> q ==> p /\ q)
by (conjt ())
let ea6' (p q r : prop) =
assert (p ==> r ==> q ==> (p /\ (q ==> r)))
by (conjt ())
let ea7' (p q r : prop) =
assert (p ==> q ==> ((r ==> p) /\ (r ==> p ==> q)))
by (conjt ())
(* Exercise: the `conjt` fails for goals such as the following. Why? Can
you fix it so it will solve it (and all previous goals?) *)
//let eb1 (p q: prop) =
// assert ((p ==> q) ==> (p ==> q))
// by (conjt ())
(* Exercise: extend `conjt` to also solve disjunctions. (Hint: use
`try..with` to backtrack.) It should solve all of the following goals.
*)
let disjt () : Tac unit = smt () (* but don't use SMT :) *)
let ea1'' (p q r : prop) =
assert (p ==> q ==> r ==> p)
by (disjt ())
let ea2'' (p q r : prop) =
assert (p ==> q ==> r ==> q)
by (disjt ())
let ea3'' (p q r : prop) =
assert (p ==> q ==> r ==> r)
by (disjt ())
let ea4'' (p q r : prop) =
assert (p ==> q ==> r ==> (forall (x:int). r))
by (disjt ())
let ea5'' (p q : prop) =
assert (p ==> q ==> p /\ q)
by (disjt ())
let ea6'' (p q r : prop) =
assert (p ==> r ==> q ==> (p /\ (q ==> r)))
by (disjt ())
let ea7'' (p q r : prop) =
assert (p ==> q ==> ((r ==> p) /\ (r ==> p ==> q)))
by (disjt ())
let ea8'' (p q : prop) =
assert (p ==> q ==> p \/ q)
by (disjt ())
let ea9'' (p q : prop) =
assert (p ==> p \/ q)
by (disjt ())
let ea10'' (p q : prop) =
assert (q ==> p \/ q)
by (disjt ())