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
|
(***********************************************************************)
(* 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 Names
open Ccalgo
type proof=
Ax of identifier
| Refl of term
| Trans of proof*proof
| Sym of proof
| Congr of proof*proof
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
| Sym p->p
| Ax s-> Sym(Ax s)
| 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)
let build_proof uf i j=
let rec equal_proof i j=
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),t)=
let pi=equal_proof i t.lhs in
let pj=psym (equal_proof j t.rhs) in
let pij=
match t.rule with
Axiom s->Ax s
| Congruence->congr_proof t.lhs t.rhs
in ptrans(ptrans (pi,pij),pj)
and path_proof i=function
[] -> let t=UF.term uf i in Refl t
| x::q->ptrans (path_proof j 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)
in
equal_proof i j
let rec type_proof axioms p=
match p with
Ax s->List.assoc s axioms
| 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 failwith "invalid transitivity"
| Sym p->let (t1,t2)=type_proof axioms p in (t2,t1)
| Congr (p1,p2)->
let (i1,j1)=type_proof axioms p1
and (i2,j2)=type_proof axioms p2 in
Appli (i1,i2),Appli (j1,j2)
let cc_proof (axioms,(v,w))=
let uf=make_uf axioms in
let i1=UF.add v uf in
let i2=UF.add w uf in
cc uf;
if UF.find uf i1=UF.find uf i2 then
let prf=build_proof uf i1 i2 in
if (v,w)=type_proof axioms prf then Some (prf,uf,axioms)
else failwith "Proof check failed !!"
else
None;;
|
