blob: 1897a8ba6f0b16ad88545109e55d1ae46fd6909f (
plain)
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
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
(*i $Id$ i*)
open Util
open Names
open Term
open Tactics
open Tacticals
open Hiddentac
open Equality
open Auto
open Pattern
open Hipattern
open Proof_trees
open Proof_type
open Tacmach
open Coqlib
(* This file containts the implementation of the tactics ``Decide
Equality'' and ``Compare''. They can be used to decide the
propositional equality of two objects that belongs to a small
inductive datatype --i.e., an inductive set such that all the
arguments of its constructors are non-functional sets.
The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as
follows:
1. Eliminate x and then y.
2. Try discrimination to solve those goals where x and y has
been introduced by different constructors.
3. If x and y have been introduced by the same constructor,
then analyse one by one the correspoing pairs of arguments.
If they are equal, rewrite one into the other. If they are
not, derive a contradiction from the injectiveness of the
constructor.
4. Once all the arguments have been rewritten, solve the left half
of the disjunction by reflexivity.
Eduardo Gimenez (30/3/98).
*)
let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
let mkBranches =
(tclTHEN intro
(tclTHEN (tclLAST_HYP h_simplest_elim)
(tclTHEN clear_last
(tclTHEN intros
(tclTHEN (tclLAST_HYP h_simplest_case)
(tclTHEN clear_last
intros))))))
let solveRightBranch = (tclTHEN h_simplest_right h_discrConcl)
let h_solveRightBranch =
hide_atomic_tactic "solveRightBranch" solveRightBranch
(* Constructs the type {c1=c2}+{~c1=c2} *)
let mkDecideEqGoal rectype c1 c2 g =
let equality = mkAppA [|build_coq_eq_data.eq (); rectype; c1; c2|] in
let disequality = mkAppA [|build_coq_not (); equality|] in
mkAppA [|build_coq_sumbool (); equality; disequality |]
(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
let mkGenDecideEqGoal rectype g =
let hypnames = pf_ids_of_hyps g in
let xname = next_ident_away (id_of_string "x") hypnames
and yname = next_ident_away (id_of_string "y") hypnames in
(mkNamedProd xname rectype
(mkNamedProd yname rectype
(mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
let eqCase tac =
(tclTHEN intro
(tclTHEN (tclLAST_HYP h_rewriteLR)
(tclTHEN clear_last
tac)))
let diseqCase =
let diseq = id_of_string "diseq" in
let absurd = id_of_string "absurd" in
(tclTHEN (intro_using diseq)
(tclTHEN h_simplest_right
(tclTHEN red_in_concl
(tclTHEN (intro_using absurd)
(tclTHEN (h_simplest_apply (mkVar diseq))
(tclTHEN (h_injHyp absurd)
full_trivial))))))
let solveArg a1 a2 tac g =
let rectype = pf_type_of g a1 in
let decide = mkDecideEqGoal rectype a1 a2 g in
(tclTHENS
(h_elimType decide)
[(eqCase tac);diseqCase;default_auto]) g
let solveLeftBranch rectype g =
match
try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g)
with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
with
| _ :: lhs :: rhs :: _ ->
let nparams = Global.mind_nparams rectype in
let getargs l = snd (list_chop nparams (snd (decomp_app l))) in
let rargs = getargs (snd rhs)
and largs = getargs (snd lhs) in
List.fold_right2
solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
| _ -> anomaly "Unexpected pattern for solveLeftBranch"
(* The tactic Decide Equality *)
let hd_app c = match kind_of_term c with
| IsApp (h,_) -> h
| _ -> c
let decideGralEquality g =
match
try matches (build_coq_eqdec_pattern ()) (pf_concl g)
with Pattern.PatternMatchingFailure ->
error "The goal does not have the expected form"
with
| (_,typ) :: _ ->
let headtyp = hd_app (pf_compute g typ) in
let rectype =
match kind_of_term headtyp with
| IsMutInd mi -> mi
| _ -> error
"This decision procedure only works for inductive objects"
in
(tclTHEN
mkBranches
(tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
| _ -> anomaly "Unexpected pattern for decideGralEquality"
let decideEquality c1 c2 g =
let rectype = (pf_type_of g c1) in
let decide = mkGenDecideEqGoal rectype g in
(tclTHENS (cut decide) [default_auto;decideGralEquality]) g
(* The tactic Compare *)
let compare c1 c2 g =
let rectype = pf_type_of g c1 in
let decide = mkDecideEqGoal rectype c1 c2 g in
(tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (tclLAST_HYP simplest_case)
clear_last));
decideEquality c1 c2]) g
(* The dynamic tactics to be registered in the tactics table *)
let dyn_decideEquality args g = match args with
| [ Constr c1; Constr c2 ] ->
decideEquality c1 c2 g
| [ Command com1; Command com2 ] ->
let c1 = pf_interp_constr g com1
and c2 = pf_interp_constr g com2 in
decideEquality c1 c2 g
| [] -> decideGralEquality g
| _ -> error "Invalid arguments for dynamic tactic"
let dyn_compare args g = match args with
| [ Constr c1; Constr c2 ] ->
compare c1 c2 g
| [ Command com1; Command com2 ] ->
let c1 = pf_interp_constr g com1
and c2 = pf_interp_constr g com2 in
compare c1 c2 g
| _ -> error "Invalid arguments for dynamic tactic"
(* Tactic registration *)
let _ = add_tactic "DecideEquality" dyn_decideEquality
let _ = add_tactic "Compare" dyn_compare
|
