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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
open Util
open Names
open Ccalgo
type proof=
Ax of identifier
| SymAx of identifier
| Refl of term
| Trans of proof*proof
| Congr of proof*proof
| Inject of proof*constructor*int*int
let pcongr=function
Refl t1, Refl t2 -> Refl (Appli (t1,t2))
| p1, p2 -> Congr (p1,p2)
let rec ptrans=function
Refl _, p ->p
| p, Refl _ ->p
| Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3))
| Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4))
| Congr(p1,p2), Trans(Congr(p3,p4),p5) ->
ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
| p1, p2 ->Trans (p1,p2)
let rec psym=function
Refl p->Refl p
| SymAx s->Ax s
| Ax s-> SymAx s
| Inject (p,c,n,a)-> Inject (psym p,c,n,a)
| Trans (p1,p2)-> ptrans (psym p2,psym p1)
| Congr (p1,p2)-> pcongr (psym p1,psym p2)
let pcongr=function
Refl t1, Refl t2 ->Refl (Appli (t1,t2))
| p1, p2 -> Congr (p1,p2)
type ('a,'b) mission=
Prove of 'a
| Refute of 'b
let build_proof uf=
let rec equal_proof i j=
if i=j then Refl (UF.term uf i) else
let (li,lj)=UF.join_path uf i j in
ptrans (path_proof i li,psym (path_proof j lj))
and edge_proof ((i,j),eq)=
let pi=equal_proof i eq.lhs in
let pj=psym (equal_proof j eq.rhs) in
let pij=
match eq.rule with
Axiom s->Ax s
| Congruence ->congr_proof eq.lhs eq.rhs
| Injection (ti,tj,c,a) ->
let p=equal_proof ti tj in
let p1=constr_proof ti ti c 0
and p2=constr_proof tj tj c 0 in
match UF.term uf c with
Constructor (cstr,nargs,nhyps) ->
Inject(ptrans(psym p1,ptrans(p,p2)),cstr,nhyps,a)
| _ -> anomaly "injection on non-constructor terms"
in ptrans(ptrans (pi,pij),pj)
and constr_proof i j c n=
try
let nj=UF.mem_node_pac uf j (c,n) in
let (ni,arg)=UF.subterms uf j in
let p=constr_proof ni nj c (n+1) in
let targ=UF.term uf arg in
ptrans (equal_proof i j, pcongr (p,Refl targ))
with Not_found->equal_proof i j
and path_proof i=function
[] -> Refl (UF.term uf i)
| x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x)
and congr_proof i j=
let (i1,i2) = UF.subterms uf i
and (j1,j2) = UF.subterms uf j in
pcongr (equal_proof i1 j1, equal_proof i2 j2)
and discr_proof i ci j cj=
let p=equal_proof i j
and p1=constr_proof i i ci 0
and p2=constr_proof j j cj 0 in
ptrans(psym p1,ptrans(p,p2))
in
function
Prove(i,j)-> equal_proof i j
| Refute(i,ci,j,cj)-> discr_proof i ci j cj
let rec nth_arg t n=
match t with
Appli (t1,t2)->
if n>0 then
nth_arg t1 (n-1)
else t2
| _ -> anomaly "nth_arg: not enough args"
let rec type_proof axioms p=
match p with
Ax s->List.assoc s axioms
| SymAx s-> let (t1,t2)=List.assoc s axioms in (t2,t1)
| Refl t-> t,t
| Trans (p1,p2)->
let (s1,t1)=type_proof axioms p1
and (t2,s2)=type_proof axioms p2 in
if t1=t2 then (s1,s2) else anomaly "invalid cc transitivity"
| Congr (p1,p2)->
let (i1,j1)=type_proof axioms p1
and (i2,j2)=type_proof axioms p2 in
Appli (i1,i2),Appli (j1,j2)
| Inject (p,c,n,a)->
let (ti,tj)=type_proof axioms p in
nth_arg ti (n-a),nth_arg tj (n-a)
let cc_proof (axioms,m)=
try
let uf=make_uf axioms in
match m with
Some (v,w) ->
let i1=UF.add uf v in
let i2=UF.add uf w in
cc uf;
if UF.find uf i1=UF.find uf i2 then
let prf=build_proof uf (Prove(i1,i2)) in
if (v,w)=type_proof axioms prf then
Prove (prf,axioms)
else anomaly "wrong proof generated"
else
errorlabstrm "CC" (Pp.str "CC couldn't solve goal")
| None ->
cc uf;
errorlabstrm "CC" (Pp.str "CC couldn't solve goal")
with UF.Discriminable (i,ci,j,cj,uf) ->
let prf=build_proof uf (Refute(i,ci,j,cj)) in
let (t1,t2)=type_proof axioms prf in
Refute (t1,t2,prf,axioms)
|
