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
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
open CErrors
open Constr
open Ccalgo
open Pp
type rule=
Ax of constr
| SymAx of constr
| Refl of term
| Trans of proof*proof
| Congr of proof*proof
| Inject of proof*pconstructor*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 term_equal p1.p_rhs p3.p_lhs then
{p_lhs=p1.p_lhs;
p_rhs=p3.p_rhs;
p_rule=Trans (p1,p3)}
else anomaly (Pp.str "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 = Constrhash.find axioms s in
{p_lhs=l;
p_rhs=r;
p_rule=Ax s}
let psymax axioms s =
let l,r = Constrhash.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 ~label:"nth_arg" (Pp.str "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 rec equal_proof uf i j=
debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
if i=j then prefl (term uf i) else
let (li,lj)=join_path uf i j in
ptrans (path_proof uf i li) (psym (path_proof uf j lj))
and edge_proof uf ((i,j),eq)=
debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let pi=equal_proof uf i eq.lhs in
let pj=psym (equal_proof uf j eq.rhs) in
let pij=
match eq.rule with
Axiom (s,reversed)->
if reversed then psymax (axioms uf) s
else pax (axioms uf) s
| Congruence ->congr_proof uf eq.lhs eq.rhs
| Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *)
let p=ind_proof uf 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 uf i ipac=
debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
let t=find_oldest_pac uf i ipac in
let eq_it=equal_proof uf i t in
if ipac.args=[] then
eq_it
else
let fipac=tail_pac ipac in
let (fi,arg)=subterms uf t in
let targ=term uf arg in
let p=constr_proof uf fi fipac in
ptrans eq_it (pcongr p (prefl targ))
and path_proof uf i l=
debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
(prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
match l with
| [] -> prefl (term uf i)
| x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
and congr_proof uf i j=
debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
and ind_proof uf i ipac j jpac=
debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let p=equal_proof uf i j
and p1=constr_proof uf i ipac
and p2=constr_proof uf j jpac in
ptrans (psym p1) (ptrans p p2)
let build_proof uf=
function
| `Prove (i,j) -> equal_proof uf i j
| `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj