...
 
Commits (20)
......@@ -417,12 +417,14 @@ PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUG_MICROC = mc_ast mc_parser mc_lexer mc_main
PLUG_CERTD = certd_syntax certd_verif certd_transformations certd_register
PLUGINS = genequlin dimacs tptp python microc
PLUGINS = genequlin dimacs tptp python microc certd
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
CERTDMODULES = $(addprefix plugins/certd/, $(PLUG_CERTD))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
......@@ -433,6 +435,9 @@ PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
CERTDCMO = $(addsuffix .cmo, $(CERTDMODULES))
CERTDCMX = $(addsuffix .cmx, $(CERTDMODULES))
ifeq (@enable_hypothesis_selection@,yes)
PLUG_TRANSFORM += hypothesis_selection
PLUGINS += hypothesis_selection
......@@ -446,13 +451,13 @@ endif
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES)
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES) $(CERTDMODULES)
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGDIRS = parser printer transform tptp python microc
PLUGDIRS = parser printer transform tptp python microc certd
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
......@@ -489,6 +494,8 @@ lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
lib/plugins/microc.cmxs: $(MICROCCMX)
lib/plugins/microc.cmo: $(MICROCCMO)
lib/plugins/certd.cmxs: $(CERTDCMX)
lib/plugins/certd.cmo: $(CERTDCMO)
# depend and clean targets
......
Term : Type.
Prop : Type.
def prf : Prop -> Type.
true : Prop.
false: Prop.
not : Prop -> Prop.
and : Prop -> Prop -> Prop.
or : Prop -> Prop -> Prop.
imp : Prop -> Prop -> Prop.
forall: (Term -> Prop) -> Prop.
exists: (Term -> Prop) -> Prop.
equals: Term -> Term -> Prop.
def equiv: Prop -> Prop -> Prop := A: Prop => B: Prop => and (imp A B) (imp B A).
tt: prf true.
[] prf false --> P: Prop -> prf P
[A] prf (not A) --> prf A -> prf false
[A,B] prf (and A B) --> P: Prop -> (prf A -> prf B -> prf P) -> prf P
[A,B] prf (or A B) --> P: Prop -> (prf A -> prf P) -> (prf B -> prf P) -> prf P
[A,B] prf (imp A B) --> prf A -> prf B
[A] prf (forall A) --> x: Term -> prf (A x)
[A] prf (exists A) --> P: Prop -> (x: Term -> prf (A x) -> prf P) -> prf P
[x,y] prf (equals x y) --> P: (Term -> Prop) -> prf (P x) -> prf (P y).
(; Define sequents. The sequent <A, B ⊢ C, D> is represented by < A → B → ¬C → ¬ D → ⊥ > ;)
def empty : Prop
:= false.
def hyp : Prop -> Prop -> Prop
:= A => s => imp A s.
def goal : Prop -> Prop -> Prop
:= A => s => imp (not A) s.
(; classical axiom and reasoning about negation ;)
def iff : A : Prop -> B : Prop -> Prop
:= A => B => and (imp A B) (imp B A).
def nni (A : Prop) :
prf A -> prf (not (not A))
:= a => na => na a.
def contra (A : Prop) (B : Prop) :
(prf A -> prf B) ->
prf (not B) -> prf (not A)
:= p => nb => a => nb (p a).
tnd : A : Prop -> prf (or A (not A)).
def nne : A : Prop -> prf (not (not A)) -> prf A
:= A : Prop => nna =>
tnd A A (a => a) (na => nna na A).
(; *** Theorems ;)
(; implication ;)
def imp_elim : A: Prop -> B: Prop -> prf (imp A B) -> prf A -> prf B
:= A: Prop => B: Prop => p: prf (imp A B) => p.
def imp_intro : A: Prop -> B: Prop -> (prf A -> prf B) -> prf (imp A B)
:= A: Prop => B: Prop => p: (prf A -> prf B) => p.
(; disjunction ;)
def or_intro_1 : A: Prop -> B: Prop -> prf A -> prf (or A B)
:= A: Prop => B: Prop => p: prf A =>
P: Prop => f: (prf A -> prf P) => g: (prf B -> prf P) => f p.
def or_intro_2 : A: Prop -> B: Prop -> prf B -> prf (or A B)
:= A: Prop => B: Prop => p: prf B =>
P: Prop => f: (prf A -> prf P) => g: (prf B -> prf P) => g p.
def or_elim : A: Prop -> B: Prop -> prf (or A B) -> C: Prop -> prf (imp A C) -> prf (imp B C) -> prf C
:= A: Prop => B: Prop => p: prf (or A B) => p.
(; conjunction ;)
def and_intro : A: Prop -> B: Prop -> prf A -> prf B -> prf (and A B)
:= A: Prop => B: Prop => a: prf A => b: prf B => P: Prop => f: (prf A -> prf B -> prf P) => f a b.
def and_elim_1 : A: Prop -> B: Prop -> prf (and A B) -> prf A
:= A: Prop => B: Prop => p: prf (and A B) => p A (a: prf A => b: prf B => a).
def and_elim_2 : A: Prop -> B: Prop -> prf (and A B) -> prf B
:= A: Prop => B: Prop => p: prf (and A B) => p B (a: prf A => b: prf B => b).
(; Universal quantifier ;)
def forall_intro: P: (Term->Prop) -> (t: Term -> prf (P t)) -> prf (forall P)
:= P: (Term->Prop) => p: (t: Term -> prf (P t)) => p.
def forall_elim: P: (Term->Prop) -> t: Term -> p: prf (forall P) -> prf (P t)
:= P: (Term->Prop) => t: Term => p: prf (forall P) => p t.
(; Existential quantifier ;)
def exists_intro: P: (Term->Prop) -> t: Term -> prf (P t) -> prf (exists P)
:= P: (Term -> Prop) => t: Term => p: prf (P t) =>
A: Prop => f: (x: Term -> prf (P x) -> prf A) => f t p.
def exists_elim: P: (Term->Prop) -> Q: Prop -> prf (exists P) -> prf (forall (x => imp (P x) Q)) -> prf Q
:= P: (Term->Prop) => Q: Prop => p1: prf (exists P) => p2: prf (forall (x => imp (P x) Q))
=> p1 Q p2.
(; Equality ;)
def eq_refl: prf (forall (x: Term => equals x x))
:= x: Term => P: (Term -> Prop) => p: prf (P x) => p.
def eq_sym: prf( forall (x: Term => forall (y: Term => (imp (equals x y) (equals y x)))) )
:= x: Term => y: Term => p: prf (equals x y) => p (z: Term => equals z x) (eq_refl x).
def eq_trans: prf ( forall (x: Term => forall (y: Term => (forall (z: Term => imp (and (equals x y) (equals y z)) (equals x z))))) )
:= x: Term => y: Term => z: Term => p: prf (and (equals x y) (equals y z)) => P: (Term -> Prop) => q: prf (P x) =>
and_elim_2 (equals x y) (equals y z) p P (and_elim_1 (equals x y) (equals y z) p P q).
(; certificate lines ;)
def skip : prf false -> prf false
:= f => f.
def axiom (P : Prop) :
prf P -> prf (not P) -> prf false
:= p => np => np p.
def trivial_hyp : prf false -> prf false
:= f => f.
def trivial_goal : prf (not true) -> prf false
:= h => h tt.
def cut (A : Prop) :
prf (goal A empty) ->
prf (hyp A empty) ->
prf false
:= nna => na => nna na.
def split_hyp (A : Prop) (B : Prop) :
prf (hyp A empty) ->
prf (hyp B empty) ->
prf (hyp (or A B) empty)
:= s1 => s2 => h =>
or_elim A B h false s1 s2.
def split_goal (A : Prop) (B : Prop) :
prf (goal A empty) ->
prf (goal B empty) ->
prf (goal (and A B) empty)
:= nna => nnb => nni (and A B) (and_intro A B (nne A nna) (nne B nnb)).
def unfold_iff_hyp (A : Prop) (B : Prop) :
prf (hyp (and (imp A B) (imp B A)) empty) ->
prf (hyp (iff A B) empty)
:= h => h.
def unfold_iff_goal (A : Prop) (B : Prop) :
prf (goal (and (imp A B) (imp B A)) empty) ->
prf (goal (iff A B) empty)
:= h => h.
def unfold_arr_hyp (A : Prop) (B : Prop) :
prf (hyp (or (not A) B) empty) ->
prf (hyp (imp A B) empty)
:= h => impab =>
h (tnd A (or (not A) B) (a => or_intro_2 (not A) B (impab a))
(na => or_intro_1 (not A) B na)).
def unfold_arr_goal (A : Prop) (B : Prop) :
prf (goal (or (not A) B) empty) ->
prf (goal (imp A B) empty)
:= h => nni (imp A B) (a =>
nne (or (not A) B) h B (na => na a B)
(b => b)).
def swap_neg_neg_hyp (A : Prop) :
prf (goal A empty) ->
prf (hyp (not A) empty)
:= h => h.
def swap_neg_hyp (A : Prop) :
prf (goal (not A) empty) ->
prf (hyp A empty)
:= nnna => nne (not A) nnna.
def swap_neg_goal (A : Prop) :
prf (hyp (not A) empty) ->
prf (goal A empty)
:= h => h.
def swap_neg_neg_goal (A : Prop) :
prf (hyp A empty) ->
prf (goal (not A) empty)
:= na => nni (not A) na.
def destruct_hyp (A : Prop) (B : Prop) :
prf (hyp A (hyp B empty)) ->
prf (hyp (and A B) empty)
:= s => h =>
s (and_elim_1 A B h) (and_elim_2 A B h).
def destruct_goal (A : Prop) (B : Prop) :
prf (goal A (goal B empty)) ->
prf (goal (or A B) empty)
:= h => nab => h (a => nab (or_intro_1 A B a))
(b => nab (or_intro_2 A B b)).
def dir_left_hyp (A : Prop) (B : Prop) :
prf (hyp A empty) ->
prf (hyp (and A B) empty)
:= na => ab => na (and_elim_1 A B ab).
def dir_left_goal (A : Prop) (B : Prop) :
prf (goal A empty) ->
prf (goal (or A B) empty)
:= nna => nab => nab (or_intro_1 A B (nne A nna)).
def dir_right_hyp (A : Prop) (B : Prop) :
prf (hyp B empty) ->
prf (hyp (and A B) empty)
:= nb => ab => nb (and_elim_2 A B ab).
def dir_right_goal (A : Prop) (B : Prop) :
prf (goal B empty) ->
prf (goal (or A B) empty)
:= nnb => nab => nab (or_intro_2 A B (nne B nnb)).
def weakening_hyp (A : Prop) :
prf empty ->
prf (hyp A empty)
:= f => a => f.
def weakening_goal (A : Prop) :
prf empty ->
prf (goal A empty)
:= f => a => f.
Term : Type.
Prop : Type.
def prf : Prop -> Type.
true : Prop.
false: Prop.
not : Prop -> Prop.
and : Prop -> Prop -> Prop.
or : Prop -> Prop -> Prop.
imp : Prop -> Prop -> Prop.
forall: (Term -> Prop) -> Prop.
exists: (Term -> Prop) -> Prop.
equals: Term -> Term -> Prop.
def equiv: Prop -> Prop -> Prop := A: Prop => B: Prop => and (imp A B) (imp B A).
tt: prf true.
[] prf false --> P: Prop -> prf P
[A] prf (not A) --> prf A -> prf false
[A,B] prf (and A B) --> P: Prop -> (prf A -> prf B -> prf P) -> prf P
[A,B] prf (or A B) --> P: Prop -> (prf A -> prf P) -> (prf B -> prf P) -> prf P
[A,B] prf (imp A B) --> prf A -> prf B
[A] prf (forall A) --> x: Term -> prf (A x)
[A] prf (exists A) --> P: Prop -> (x: Term -> prf (A x) -> prf P) -> prf P
[x,y] prf (equals x y) --> P: (Term -> Prop) -> prf (P x) -> prf (P y).
(; *** Theorems ;)
(; implication ;)
def imp_elim : A: Prop -> B: Prop -> prf (imp A B) -> prf A -> prf B
:= A: Prop => B: Prop => p: prf (imp A B) => p.
def imp_intro : A: Prop -> B: Prop -> (prf A -> prf B) -> prf (imp A B)
:= A: Prop => B: Prop => p: (prf A -> prf B) => p.
(; disjunction ;)
def or_intro_1 : A: Prop -> B: Prop -> prf A -> prf (or A B)
:= A: Prop => B: Prop => p: prf A =>
P: Prop => f: (prf A -> prf P) => g: (prf B -> prf P) => f p.
def or_intro_2 : A: Prop -> B: Prop -> prf B -> prf (or A B)
:= A: Prop => B: Prop => p: prf B =>
P: Prop => f: (prf A -> prf P) => g: (prf B -> prf P) => g p.
def or_elim : A: Prop -> B: Prop -> prf (or A B) -> C: Prop -> prf (imp A C) -> prf (imp B C) -> prf C
:= A: Prop => B: Prop => p: prf (or A B) => p.
(; conjunction ;)
def and_intro : A: Prop -> B: Prop -> prf A -> prf B -> prf (and A B)
:= A: Prop => B: Prop => a: prf A => b: prf B => P: Prop => f: (prf A -> prf B -> prf P) => f a b.
def and_elim_1 : A: Prop -> B: Prop -> prf (and A B) -> prf A
:= A: Prop => B: Prop => p: prf (and A B) => p A (a: prf A => b: prf B => a).
def and_elim_2 : A: Prop -> B: Prop -> prf (and A B) -> prf B
:= A: Prop => B: Prop => p: prf (and A B) => p B (a: prf A => b: prf B => b).
(; Universal quantificator ;)
def forall_intro: P: (Term->Prop) -> (t: Term -> prf (P t)) -> prf (forall P)
:= P: (Term->Prop) => p: (t: Term -> prf (P t)) => p.
def forall_elim: P: (Term->Prop) -> t: Term -> p: prf (forall P) -> prf (P t)
:= P: (Term->Prop) => t: Term => p: prf (forall P) => p t.
(; Existential quantificator ;)
def exists_intro: P: (Term->Prop) -> t: Term -> prf (P t) -> prf (exists P)
:= P: (Term -> Prop) => t: Term => p: prf (P t) =>
A: Prop => f: (x: Term -> prf (P x) -> prf A) => f t p.
def exists_elim: P: (Term->Prop) -> Q: Prop -> prf (exists P) -> prf (forall (x => imp (P x) Q)) -> prf Q
:= P: (Term->Prop) => Q: Prop => p1: prf (exists P) => p2: prf (forall (x => imp (P x) Q))
=> p1 Q p2.
(; Equality ;)
def eq_refl: prf (forall (x: Term => equals x x))
:= x: Term => P: (Term -> Prop) => p: prf (P x) => p.
def eq_sym: prf( forall (x: Term => forall (y: Term => (imp (equals x y) (equals y x)))) )
:= x: Term => y: Term => p: prf (equals x y) => p (z: Term => equals z x) (eq_refl x).
def eq_trans: prf ( forall (x: Term => forall (y: Term => (forall (z: Term => imp (and (equals x y) (equals y z)) (equals x z))))) )
:= x: Term => y: Term => z: Term => p: prf (and (equals x y) (equals y z)) => P: (Term -> Prop) => q: prf (P x) =>
and_elim_2 (equals x y) (equals y z) p P (and_elim_1 (equals x y) (equals y z) p P q).
def split_hyp_or (a : Prop) (b : Prop) (c : Prop) (h : prf (or a b)) :
(prf a -> prf c) ->
(prf b -> prf c) ->
prf c
:= or_elim a b h c.
def split_hyp_and : (a : Prop) ->
(b : Prop) ->
(c : Prop) ->
prf (and a b) ->
(prf a -> prf b -> prf c) ->
prf c
:= a => b => c => Hab => f =>
f (and_elim_1 a b Hab) (and_elim_2 a b Hab).
#CHECK (a => b => c => d => task_1 => task_2 => h =>
split_hyp_and a (or b c) d h (ha => hbc =>
split_hyp_or b c d hbc (hb => task_1 ha hb) (hc => task_2 ha hc))) :
(a : Prop) ->
(b : Prop) ->
(c : Prop) ->
(d : Prop) ->
prf (imp (imp a (imp b d))
(imp (imp a (imp c d))
(imp (and a (or b c))
d))).
#CHECK (a => b => c => task1 => h => split_hyp_and a b c h (Hand_1 => Hand_2 => task1 Hand_2 Hand_1 )) :
((a : Prop) -> (b : Prop) -> (c : Prop) -> prf (imp (imp (b) (imp (a) (c))) (imp ((and a b)) (c)))).
(;-----------;)
(; HOL Types ;)
(;-----------;)
type : Type.
bool : type.
ind : type.
arr : type -> type -> type.
(;-----------;)
(; HOL Terms ;)
(;-----------;)
def term : type -> Type.
[a,b] term (arr a b) --> term a -> term b.
eq : a : type -> term (arr a (arr a bool)).
select : a : type -> term (arr (arr a bool) a).
(;------------;)
(; HOL Proofs ;)
(;------------;)
def proof : term bool -> Type.
REFL : a : type -> t : term a ->
proof (eq a t t).
ABS_THM : a : type -> b : type -> f : (term a -> term b) -> g : (term a -> term b) ->
(x : term a -> proof (eq b (f x) (g x))) -> proof (eq (arr a b) f g).
APP_THM : a : type -> b : type -> f : term (arr a b) -> g : term (arr a b) -> x : term a -> y : term a ->
proof (eq (arr a b) f g) ->
proof (eq a x y) ->
proof (eq b (f x) (g y)).
PROP_EXT : p : term bool -> q : term bool ->
(proof q -> proof p) ->
(proof p -> proof q) ->
proof (eq bool p q).
EQ_MP : p : term bool -> q : term bool ->
proof (eq bool p q) ->
proof p ->
proof q.
def BETA_CONV : a : type -> b : type -> f : (term a -> term b) -> u : term a ->
proof (eq b (f u) (f u)) :=
a : type => b : type => f : (term a -> term b) => u : term a =>
REFL b (f u).
def SYM (a : type) (t : term a) (u : term a) (H : proof (eq a t u)) : proof (eq a u t)
:=
EQ_MP
(eq a t t)
(eq a u t)
(APP_THM
a
bool
(eq a t)
(eq a u)
t
t
(APP_THM
a
(arr a bool)
(eq a)
(eq a)
t
u
(REFL (arr a (arr a bool)) (eq a))
H)
(REFL a t))
(REFL a t).
def TRANS (a : type) (t : term a) (u : term a) (v : term a) (H1 : proof (eq a t u)) (H2 : proof (eq a u v)) : proof (eq a t v)
:=
EQ_MP
(eq a u v)
(eq a t v)
(APP_THM
a
bool
(eq a u)
(eq a t)
v
v
(APP_THM a (arr a bool) (eq a) (eq a) u t (REFL (arr a (arr a bool)) (eq a)) (SYM a t u H1))
(REFL a v))
H2.
def PROVE_HYP (x : term bool) (y : term bool) (H1 : proof x) (H2 : proof x -> proof y) : proof y := H2 H1.
(;---------------------;)
(; Derived Connectives ;)
(;---------------------;)
def true : term bool :=
eq (arr bool bool) (p : term bool => p) (p : term bool => p).
def forall : a : type -> p : term (arr a bool) -> term bool :=
a : type => p : term (arr a bool) =>
eq (arr a bool) p (x : term a => true).
def false : term bool :=
forall bool (p : term bool => p).
def and : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
eq (arr (arr bool (arr bool bool)) bool)
(f : term (arr bool (arr bool bool)) => f p q)
(f : term (arr bool (arr bool bool)) => f true true).
def imp : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
eq bool (and p q) p.
def or : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
forall bool (r : term bool => imp (imp p r) (imp (imp q r) r)).
def cond : a : type -> term (arr bool (arr a (arr a a))) :=
a : type => t : term bool => t1 : term a => t2 : term a =>
select a (x : term a =>
and
(imp (eq bool t true) (eq a x t1))
(imp (eq bool t false) (eq a x t2))).
def not (p : term bool) :=
imp p false.
witness : a : type -> term a.
(; := a : type => select a (x : term a => true). ;)
def true_intro : proof true :=
REFL (arr bool bool) (p : term bool => p).
def eq_sym (a : type) (x : term a) (y : term a) (h : proof (eq a x y)) : proof (eq a y x) :=
EQ_MP (eq a x x) (eq a y x)
(APP_THM a bool (eq a x) (eq a y) x x
(APP_THM a (arr a bool) (eq a) (eq a) x y
(REFL (arr a (arr a bool)) (eq a))
(h))
(REFL a x))
(REFL a x).
def eq_true_intro (p : term bool) (h : proof p) : proof (eq bool p true) :=
PROP_EXT p true (h2 : proof true => h) (h : proof p => true_intro).
def eq_true_elim (p : term bool) (h : proof (eq bool p true)) : proof p :=
EQ_MP true p (eq_sym bool p true h) true_intro.
def forall_intro (a : type) (p : term (arr a bool))
(h : (x : term a -> proof (p x))) : proof (forall a p) :=
ABS_THM a bool p (x : term a => true) (x : term a =>
eq_true_intro (p x) (h x)).
def forall_elim (a : type) (p : term (arr a bool))
(h : proof (forall a p)) (x : term a) : proof (p x) :=
eq_true_elim (p x)
(APP_THM a bool p (x : term a => true) x x h (REFL a x)).
def false_elim (p : term bool) (h : proof false) : proof p :=
forall_elim bool (p : term bool => p) h p.
def and_intro (p : term bool)
(q : term bool)
(Hp : proof p)
(Hq : proof q)
: proof (and p q)
:=
ABS_THM
(arr bool (arr bool bool))
bool
(f : term (arr bool (arr bool bool)) => f p q)
(f : term (arr bool (arr bool bool)) => f true true)
(f : term (arr bool (arr bool bool)) =>
APP_THM
bool
bool
(f p)
(f true)
q
true
(APP_THM
bool
(arr bool bool)
f
f
p
true
(REFL (arr bool (arr bool bool)) f)
(eq_true_intro p Hp))
(eq_true_intro q Hq)).
def and_elim1 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof p
:=
eq_true_elim p
(APP_THM
(arr bool (arr bool bool))
bool
(f : (term bool -> term bool -> term bool) => f p q)
(f : (term bool -> term bool -> term bool) => f true true)
(x : term bool => y : term bool => x)
(x : term bool => y : term bool => x)
Hpq
(REFL (arr bool (arr bool bool)) (x : term bool => y : term bool => x))).
def and_elim2 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof q
:=
eq_true_elim q
(APP_THM
(arr bool (arr bool bool))
bool
(f : (term bool -> term bool -> term bool) => f p q)
(f : (term bool -> term bool -> term bool) => f true true)
(x : term bool => y : term bool => y)
(x : term bool => y : term bool => y)
Hpq
(REFL (arr bool (arr bool bool)) (x : term bool => y : term bool => y))).
def imp_intro (p : term bool)
(q : term bool)
(Hpq : proof p -> proof q)
: proof (imp p q)
:=
PROP_EXT (and p q) p
(Hp : proof p =>
and_intro p q Hp (Hpq Hp))
(and_elim1 p q).
def imp_elim (p : term bool)
(q : term bool)
(Hpq : proof (imp p q))
(Hp : proof p)
: proof q
:=
and_elim2 p q (EQ_MP p (and p q) (eq_sym bool (and p q) p Hpq) Hp).
def or_intro1 (p : term bool)
(q : term bool)
(Hp : proof p)
: proof (or p q)
:=
forall_intro
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
(r : term bool =>
imp_intro
(imp p r)
(imp (imp q r) r)
(H : proof (imp p r) =>
imp_intro
(imp q r)
r
(__ : proof (imp q r) =>
imp_elim p r H Hp))).
def or_intro2 (p : term bool)
(q : term bool)
(Hq : proof q)
: proof (or p q)
:=
forall_intro
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
(r : term bool =>
imp_intro
(imp p r)
(imp (imp q r) r)
(__ : proof (imp p r) =>
imp_intro
(imp q r)
r
(H : proof (imp q r) =>
imp_elim q r H Hq))).
def or_elim (p : term bool)
(q : term bool)
(r : term bool)
(Hpq : proof (or p q))
(Hpr : proof p -> proof r)
(Hqr : proof q -> proof r) : proof r
:=
imp_elim
(imp q r)
r
(imp_elim
(imp p r)
(imp (imp q r) r)
(forall_elim
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
Hpq
r)
(imp_intro p r Hpr))
(imp_intro q r Hqr).
def split_hyp_or : (a : term bool) ->
(b : term bool) ->
(c : term bool) ->
proof (or a b) ->
(proof a -> proof c) ->
(proof b -> proof c) ->
proof c
:= or_elim.
def left := (a : term bool) ->
(b : term bool) ->
proof a ->
proof (or a b).
def right := (a : term bool) ->
(b : term bool) ->
proof b ->
proof (or a b).
def split_hyp_and : (a : term bool) ->
(b : term bool) ->
(c : term bool) ->
proof (and a b) ->
(proof a -> proof b -> proof c) ->
proof c
:= a => b => c => Hab => f =>
f (and_elim1 a b Hab) (and_elim2 a b Hab).
def split_concl_and : (a : term bool) ->
(b : term bool) ->
proof a ->
proof b ->
proof (and a b)
:= and_intro.
[a,b] proof (imp a b) --> proof a -> proof b.
#INFER (a : term bool => b : term bool =>
ha : proof a =>
alpha : proof (imp a b) =>
alpha ha).
open Why3
open Certd_syntax
open Certd_transformations
open Certd_verif
(** Certified transformations *)
let checker_ctrans = checker_ctrans checker
let assumption_trans = checker_ctrans assumption
let trivial_trans = checker_ctrans trivial
let exfalso_trans = checker_ctrans exfalso
let intros_trans = checker_ctrans intros
let intuition_trans = checker_ctrans intuition
let swap_trans where = checker_ctrans (swap where)
let revert_trans ls = checker_ctrans (revert ls)
let intro_trans where = checker_ctrans (intro where)
let left_trans where = checker_ctrans (dir Left where)
let right_trans where = checker_ctrans (dir Right where)
let split_trans where = checker_ctrans (split_logic where)
let instantiate_trans t what = checker_ctrans (inst t what)
let assert_trans t = checker_ctrans (cut t)
let case_trans t = checker_ctrans (case t)
let rewrite_trans g rev where = checker_ctrans (rewrite g rev where)
let clear_trans l = checker_ctrans (clear l)
let pose_trans name t = checker_ctrans (pose name t)
(** Register certified transformations *)
let () =
let open Args_wrapper in
let open Trans in
register_transform_l "assumption_cert" (store assumption_trans)
~desc:"A certified version of coq tactic [assumption]";
register_transform_l "trivial_cert" (store trivial_trans)
~desc:"A certified version of (simplified) coq tactic [trivial]";
register_transform_l "exfalso_cert" (store exfalso_trans)
~desc:"A certified version of coq tactic [exfalso]";
register_transform_l "intros_cert" (store intros_trans)
~desc:"A certified version of coq tactic [intros]";
register_transform_l "intuition_cert" (store intuition_trans)
~desc:"A certified version of (simplified) coq tactic [intuition]";
wrap_and_register ~desc:"A certified transformation that negates \
and swaps an hypothesis from the context to the goal]"
"swap_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (swap_trans where));
wrap_and_register ~desc:"A certified transformation that generalizes a variable in the goal"
"revert_cert" (Tlsymbol (Ttrans_l))
(fun ls -> store (revert_trans ls));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [intro]"
"intro_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (intro_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [left]"
"left_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (left_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [right]"
"right_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (right_trans where));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [split]"
"split_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (split_trans where));
wrap_and_register ~desc:"A certified version of transformation instantiate"
"instantiate_cert" (Tterm (Topt ("in", Tprsymbol Ttrans_l)))
(fun t_inst where -> store (instantiate_trans t_inst where));
wrap_and_register ~desc:"A certified version of transformation rewrite"
"rewrite_cert" (Toptbool ("<-", (Tprsymbol (Topt ("in", Tprsymbol (Ttrans_l))))))
(fun rev g where -> store (rewrite_trans g rev where));
wrap_and_register ~desc:"A certified version of transformation assert"
"assert_cert" (Tformula Ttrans_l)
(fun t -> store (assert_trans t));
wrap_and_register ~desc:"A certified version of transformation case"
"case_cert" (Tformula Ttrans_l)
(fun t -> store (case_trans t));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [clear]"
"clear_cert" (Tprlist Ttrans_l)
(fun l -> store (clear_trans l));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [pose]"
"pose_cert" (Tstring (Tformula Ttrans_l))
(fun name t -> store (pose_trans name t))
open Why3
open Task
open Term
open Decl
open Theory
open Ident
(** To certify transformations, we will represent Why3 tasks by the type <ctask>
and we equip transformations with a certificate <certif> *)
type cterm =
| CTbvar of int (* bound variables use De Bruijn indices *)
| CTfvar of ident (* free variables use a name *)
| CTapp of cterm * cterm
| CTbinop of binop * cterm * cterm (* application of a binary operator *)
| CTquant of quant * cterm (* forall binding *)
| CTnot of cterm
| CTtrue
| CTfalse
type ctask = (cterm * bool) Mid.t
(* We will denote a ctask <M> by <Γ ⊢ Δ> where :
• <Γ> contains all the declarations <H : P> where <H> is mapped to <(P, false)> in <M>
• <Δ> contains all the declarations <H : P> where <H> is mapped to <(P, true)> in <M>
*)
type dir = Left | Right
type path = dir list
type certif = rule * ident
(* The ident indicates where to apply the rule.
In the following rules, we will call it <G> *)
(* Replaying a certif <cert> against a ctask <cta> will be denoted <cert ⇓ cta>,
it is defined as the function <Cert_verif.check_certif> *)
and rule =
| Skip
(* Skip ⇓ (Γ ⊢ Δ) ≜ [Γ ⊢ Δ] *)
| Axiom of ident
(* Axiom H ⇓ (Γ, H : P ⊢ Δ, G : P) ≜ [] *)
| Trivial
(* Trivial ⇓ (Γ, G : false ⊢ Δ) ≜ [] *)
(* Trivial ⇓ (Γ ⊢ Δ, G : true ) ≜ [] *)
| Cut of cterm * certif * certif
(* Cut (A, c₁, c₂) ⇓ (Γ ⊢ Δ) ≜ (c₁ ⇓ (Γ ⊢ Δ, G : A)) @ (c₂ ⇓ (Γ, G : A ⊢ Δ)) *)
| Split of certif * certif
(* Split (c₁, c₂) ⇓ (Γ, G : A ∨ B ⊢ Δ) ≜ (c₁ ⇓ (Γ, G : A ⊢ Δ)) @ (c₂ ⇓ (Γ, G : B ⊢ Δ)) *)
(* Split (c₁, c₂) ⇓ (Γ ⊢ Δ, G : A ∧ B) ≜ (c₁ ⇓ (Γ ⊢ Δ, G : A)) @ (c₂ ⇓ (Γ ⊢ Δ, G : B)) *)
| Unfold of certif
(* Unfold c ⇓ (Γ, G : A ↔ B ⊢ Δ) ≜ c ⇓ (Γ, G : (A → B) ∧ (B → A) ⊢ Δ) *)
(* Unfold c ⇓ (Γ ⊢ Δ, G : A ↔ B) ≜ c ⇓ (Γ ⊢ Δ, G : (A → B) ∧ (B → A)) *)
(* Unfold c ⇓ (Γ, G : A → B ⊢ Δ) ≜ c ⇓ (Γ, G : ¬A ∨ B ⊢ Δ)*)
(* Unfold c ⇓ (Γ ⊢ Δ, G : A → B) ≜ c ⇓ (Γ ⊢ Δ, G : ¬A ∨ B)*)
| Swap_neg of certif
(* Swap_neg c ⇓ (Γ, G : ¬A ⊢ Δ) ≜ c ⇓ (Γ ⊢ Δ, G : A) *)
(* Swap_neg c ⇓ (Γ, G : A ⊢ Δ ) ≜ c ⇓ (Γ ⊢ Δ, G : ¬A) *)
(* Swap_neg c ⇓ (Γ ⊢ Δ, G : A ) ≜ c ⇓ (Γ, G : ¬A ⊢ Δ) *)
(* Swap_neg c ⇓ (Γ ⊢ Δ, G : ¬A) ≜ c ⇓ (Γ, G : A ⊢ Δ) *)
| Destruct of ident * ident * certif
(* Destruct (H₁, H₂, c) ⇓ (Γ, G : A ∧ B ⊢ Δ) ≜ c ⇓ (Γ, H₁ : A, H₂ : B ⊢ Δ) *)
(* Destruct (H₁, H₂, c) ⇓ (Γ ⊢ Δ, G : A ∨ B) ≜ c ⇓ (Γ ⊢ Δ, H₁ : A, H₂ : B) *)
| Dir of dir * certif
(* Dir (Left, c) ⇓ (Γ, G : A ∧ B ⊢ Δ) ≜ c ⇓ (Γ, G : A ⊢ Δ) *)
(* Dir (Left, c) ⇓ (Γ ⊢ Δ, G : A ∨ B) ≜ c ⇓ (Γ ⊢ Δ, G : A) *)
(* and similar definition for Right instead of Left *)
| Weakening of certif
(* Weakening c ⇓ (Γ, G : A ⊢ Δ) ≜ c ⇓ (Γ ⊢ Δ) *)
(* Weakening c ⇓ (Γ ⊢ Δ, G : A) ≜ c ⇓ (Γ ⊢ Δ) *)
| Intro_quant of ident * certif
(* Intro_quant (y, c) ⇓ (Γ, G : ∃ x. P x ⊢ Δ) ≜ c ⇓ (Γ, G : P y ⊢ Δ) (y fresh) *)
(* Intro_quant (y, c) ⇓ (Γ ⊢ Δ, G : ∀ x. P x) ≜ c ⇓ (Γ ⊢ Δ, G : P y) (y fresh) *)
| Inst_quant of ident * cterm * certif
(* Inst_quant (H, t, c) ⇓ (Γ ⊢ Δ, G : ∃ x. P x) ≜ c ⇓ (Γ ⊢ Δ, G : ∃ x. P x, H : P t) *)
(* Inst_quant (H, t, c) ⇓ (Γ, G : ∀ x. P x ⊢ Δ) ≜ c ⇓ (Γ, G : ∀ x. P x, H : P t ⊢ Δ) *)
| Revert of ident * certif (* derived from Inst_quant *)
(* Revert (x, c) ⇓ (Γ, G : P x ⊢ Δ) ≜ c ⇓ (Γ, G : ∃ y. P y ⊢ Δ) *)
(* Revert (x, c) ⇓ (Γ ⊢ Δ, G : P x) ≜ c ⇓ (Γ ⊢ Δ, G : ∀ y. P y) *)
| Rewrite of ident * path * bool * certif list
(* Rewrite (H, path, rev, lc) ⇓ Seq is defined as follows :
it tries to rewrite in <G> an equality that is in <H>, following the path <path>,
<rev> indicates if it rewrites from left to right or from right to left.
Since <H> can have premises, those are then matched against the certificates <lc> *)
let skip = Skip, id_register (id_fresh "dummy_skip_ident")
(** Translating a Why3 <task> into a <ctask> *)
let rec translate_term_rec bv_lvl lvl t =
(* level <lvl> is the number of forall above in the whole term *)
(* <bv_lvl> is mapping bound variables to their respective level *)
match t.t_node with
| Tvar v ->
let ids = v.vs_name in
begin match Mid.find_opt ids bv_lvl with
| None -> CTfvar ids
| Some lvl_s ->
assert (lvl_s <= lvl); (* a variable should not be above its definition *)
CTbvar (lvl - lvl_s)
end
| Tapp (ls, lt) ->
let ids = ls.ls_name in
let vs = match Mid.find_opt ids bv_lvl with
| None -> CTfvar ids
| Some lvl_s ->
assert (lvl_s <= lvl); (* a variable should not be above its definition *)
CTbvar (lvl - lvl_s) in
List.fold_left (fun acc t -> CTapp (acc, translate_term_rec bv_lvl lvl t))
vs lt
| Tbinop (op, t1, t2) ->
let ct1 = translate_term_rec bv_lvl lvl t1 in
let ct2 = translate_term_rec bv_lvl lvl t2 in
CTbinop (op, ct1, ct2)
| Tquant (q, tq) ->
let vs, _, t = t_open_quant tq in
assert (List.length vs = 1);
let ids = (List.hd vs).vs_name in
let lvl = lvl + 1 in
let ctq = translate_term_rec (Mid.add ids lvl bv_lvl) lvl t in
CTquant (q, ctq)
| Tnot t -> CTnot (translate_term_rec bv_lvl lvl t)
| Ttrue -> CTtrue
| Tfalse -> CTfalse
| Tconst _ -> invalid_arg "Cert_syntax.translate_term Tconst"
| Tif _ -> invalid_arg "Cert_syntax.translate_term Tif"
| Tlet _ -> invalid_arg "Cert_syntax.translate_term Tlet"
| Tcase _ -> invalid_arg "Cert_syntax.translate_term Tcase"
| Teps _ -> invalid_arg "Cert_syntax.translate_term Teps"
let translate_term t = translate_term_rec Mid.empty 0 t
let translate_decl decl =
match decl.d_node with
| Dprop (Pgoal, pr, t) ->
Mid.singleton pr.pr_name (translate_term t, true)
| Dprop (_, pr, t) ->
Mid.singleton pr.pr_name (translate_term t, false)
| _ -> Mid.empty
let translate_tdecl td =
match td.td_node with
| Decl decl -> translate_decl decl
| _ -> Mid.empty
let rec translate_task_acc acc = function
| Some {task_decl = td; task_prev = task} ->
let new_acc = Mid.set_union acc (translate_tdecl td) in
translate_task_acc new_acc task
| None -> acc
let translate_task task =
translate_task_acc Mid.empty task
(** We equip existing transformations with a certificate <certif> *)
type ctrans = task -> task list * certif
exception Certif_verification_failed of string
let verif_failed s = raise (Certif_verification_failed s)
(** Create a certified transformation from a transformation with a certificate *)
let checker_ctrans checker (ctr : ctrans) init_t =
let res_t, certif = ctr init_t in
checker certif init_t res_t
This diff is collapsed.
This diff is collapsed.
predicate a
predicate b
predicate c
predicate d
predicate e
predicate f
axiom A : a
axiom B : b
predicate p (x : bool)
goal G1 : a /\ b
goal G2 : (a /\ b) /\ (a /\ a /\ a /\ b)
goal G3 : (b /\ a) /\ ( (a /\ a) /\ c)
goal G4 : a /\ (b \/ d)
goal G5 : (a \/ c) /\ (d \/ b)
goal G6 : a /\ (c \/ d)
goal G7 : (a /\ (d \/ c) ) \/ ( ((a /\ b) /\ ((b /\ (d \/ e \/ a)) \/d)) \/ (a /\ c) )
goal G8 : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\ ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))))
goal G9 : c /\ (d \/ f) <-> (c /\ d) \/ (c /\ f)
goal G10 : c -> d
goal G11 : a /\ (d -> d)
goal G12 : (c <-> a) -> (d \/ c)
goal G13 : (c <-> d) -> c -> d
goal G14 : (d <-> c) -> c -> d
goal G15 : (a -> b -> d <-> c) -> c -> d
goal G16 : d \/ c -> c
goal G17 : (d <-> a) -> d
goal G18 : a -> d -> b -> c -> a -> d
goal G19 : forall x. (forall u. u <-> a) -> (x <-> x)
goal G20 : exists x : bool. p x -> (forall y. p y)
goal G21 : true
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file>
<path name=".."/><path name="tests.mlw"/>
<theory name="Top">
<goal name="G1" proved="true">
<transf name="assert" arg1="(forall x. p x)">
<goal name="G1.0" expl="asserted formula">
</goal>
<goal name="G1.1">
</goal>
</transf>
<transf name="assert_cert" arg1="a">
<goal name="G1.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G1.1">
</goal>
</transf>
<transf name="case_cert" arg1="true">
<goal name="G1.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G1.1">
<proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
<transf name="split_all_full" proved="true" >
<goal name="G1.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G1.1" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="G2">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G3">
<transf name="intuition_cert" >
<goal name="G3.0">
<transf name="assert_cert" arg1="true">
<goal name="G3.0.0">
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
<goal name="G3.0.1">
<transf name="exfalso_cert" >
<goal name="G3.0.1.0">
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G4">
<transf name="case_cert" arg1="true">
<goal name="G4.0">
</goal>
<goal name="G4.1">
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G5">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G6">
<transf name="intuition_cert" >
<goal name="G6.0">
</goal>
</transf>
</goal>
<goal name="G7">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G8">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G9">
<transf name="intuition_cert" >
<goal name="G9.0">
</goal>
<goal name="G9.1">
</goal>
<goal name="G9.2">
</goal>
</transf>
</goal>
<goal name="G10">
<transf name="intro_cert" >
<goal name="G10.0">
</goal>
</transf>
</goal>
<goal name="G11">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G12">
<transf name="intro_cert" >
<goal name="G12.0">
<transf name="rewrite_cert" arg1="H">
<goal name="G12.0.0">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G13">
<transf name="intros_cert" >
<goal name="G13.0">
<transf name="rewrite_cert" arg1="H1" arg2="in" arg3="H">
<goal name="G13.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G14">
<transf name="intros_cert" >
<goal name="G14.0">
<transf name="rewrite_cert" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G14.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G15">
<transf name="intros_cert" >
<goal name="G15.0">
<transf name="rewrite" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0">
</goal>
<goal name="G15.0.1" expl="rewrite premises">
</goal>
<goal name="G15.0.2" expl="rewrite premises">
</goal>
</transf>
<transf name="rewrite_cert" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.1" expl="rewrite premises">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.2" expl="rewrite premises">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G16">
<transf name="intro_cert" >
<goal name="G16.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G16.0.0">
</goal>
<goal name="G16.0.1">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G17">
<transf name="intro_cert" >
<goal name="G17.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G17.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G18">
<transf name="intros_cert" >
<goal name="G18.0">
<transf name="clear_cert" arg1="H4,H2,H1,H,A,B">
<goal name="G18.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G19">
<transf name="introduce_premises" >
<goal name="G19.0">
<transf name="revert_cert" arg1="x">
<goal name="G19.0.0">
</goal>
</transf>
<transf name="rewrite" arg1="H">
<goal name="G19.0.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20">
<transf name="case_cert" arg1="(exists x. not p x)">
<goal name="G20.0">
<transf name="intro_cert" arg1="in" arg2="H">
<goal name="G20.0.0">
<transf name="instantiate_cert" arg1="x">
<goal name="G20.0.0.0">
<transf name="intro_cert" >
<goal name="G20.0.0.0.0">
<transf name="swap_cert" arg1="in" arg2="H2">
<goal name="G20.0.0.0.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20.1">
<transf name="instantiate_cert" arg1="True">
<goal name="G20.1.0">
<transf name="intros_cert" >
<goal name="G20.1.0.0">
<transf name="swap_cert" >
<goal name="G20.1.0.0.0">
<transf name="swap_cert" arg1="in" arg2="H3">
<goal name="G20.1.0.0.0.0">
<transf name="instantiate_cert" arg1="y">
<goal name="G20.1.0.0.0.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G21">
<transf name="pose_cert" arg1="hh" arg2="true">
<goal name="G21.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -71,6 +71,9 @@ let fold_product_l f acc ll =
let flatten_rev fl =
List.fold_left (fun acc l -> List.rev_append l acc) [] fl
let rev_flatten fl =
List.fold_left (fun acc l -> l @ acc) [] fl
let part cmp l =
let l = List.stable_sort cmp l in
match l with
......
......@@ -43,6 +43,8 @@ val fold_product_l : ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
val flatten_rev : 'a list list -> 'a list
val rev_flatten : 'a list list -> 'a list
val part : ('a -> 'a -> int) -> 'a list -> 'a list list
(** [part cmp l] returns the list of the congruence classes with
respect to [cmp]. They are returned in reverse order *)
......