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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \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 Term
open Ccalgo
type rule=
Ax of constr
| SymAx of constr
| Refl of term
| Trans of proof*proof
| Congr of proof*proof
| Inject of proof*constructor*int*int
and proof =
{p_lhs:term;p_rhs:term;p_rule:rule}
let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
let pcongr p1 p2 =
match p1.p_rule,p2.p_rule with
Refl t1, Refl t2 -> prefl (Appli (t1,t2))
| _, _ ->
{p_lhs=Appli (p1.p_lhs,p2.p_lhs);
p_rhs=Appli (p1.p_rhs,p2.p_rhs);
p_rule=Congr (p1,p2)}
let rec ptrans p1 p3=
match p1.p_rule,p3.p_rule with
Refl _, _ ->p3
| _, Refl _ ->p1
| Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
| Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
| Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
| _, _ ->
if p1.p_rhs = p3.p_lhs then
{p_lhs=p1.p_lhs;
p_rhs=p3.p_rhs;
p_rule=Trans (p1,p3)}
else anomaly "invalid cc transitivity"
let rec psym p =
match p.p_rule with
Refl _ -> p
| SymAx s ->
{p_lhs=p.p_rhs;
p_rhs=p.p_lhs;
p_rule=Ax s}
| Ax s->
{p_lhs=p.p_rhs;
p_rhs=p.p_lhs;
p_rule=SymAx s}
| Inject (p0,c,n,a)->
{p_lhs=p.p_rhs;
p_rhs=p.p_lhs;
p_rule=Inject (psym p0,c,n,a)}
| Trans (p1,p2)-> ptrans (psym p2) (psym p1)
| Congr (p1,p2)-> pcongr (psym p1) (psym p2)
let pax axioms s =
let l,r = Hashtbl.find axioms s in
{p_lhs=l;
p_rhs=r;
p_rule=Ax s}
let psymax axioms s =
let l,r = Hashtbl.find axioms s in
{p_lhs=r;
p_rhs=l;
p_rule=SymAx s}
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 pinject p c n a =
{p_lhs=nth_arg p.p_lhs (n-a);
p_rhs=nth_arg p.p_rhs (n-a);
p_rule=Inject(p,c,n,a)}
let build_proof uf=
let axioms = axioms uf in
let rec equal_proof i j=
if i=j then prefl (term uf i) else
let (li,lj)=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,reversed)->
if reversed then psymax axioms s
else pax axioms s
| Congruence ->congr_proof eq.lhs eq.rhs
| Injection (ti,ipac,tj,jpac,k) ->
let p=ind_proof ti ipac tj jpac in
let cinfo= get_constructor_info uf ipac.cnode in
pinject p cinfo.ci_constr cinfo.ci_nhyps k
in ptrans (ptrans pi pij) pj
and constr_proof i t ipac=
if ipac.args=[] then
equal_proof i t
else
let npac=tail_pac ipac in
let (j,arg)=subterms uf t in
let targ=term uf arg in
let rj=find uf j in
let u=find_pac uf rj npac in
let p=constr_proof j u npac in
ptrans (equal_proof i t) (pcongr p (prefl targ))
and path_proof i=function
[] -> prefl (term uf i)
| x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
and congr_proof i j=
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
pcongr (equal_proof i1 j1) (equal_proof i2 j2)
and ind_proof i ipac j jpac=
let p=equal_proof i j
and p1=constr_proof i i ipac
and p2=constr_proof j j jpac in
ptrans (psym p1) (ptrans p p2)
in
function
`Prove (i,j) -> equal_proof i j
| `Discr (i,ci,j,cj)-> ind_proof i ci j cj
|
