Commit 38a29ea8 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Initial commit

This corresponds to my presentation at
LSV (http://deducteam.gforge.inria.fr/seminars/170302.html). The
manual is still incomplete.
parents
.config_vars
*/*.dko
*/*.dk.depend
-include .config_vars
SUBDIRS= fol meta # example
all:
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
done
clean:
for d in $(SUBDIRS); do\
$(MAKE) clean -C $$d; \
done
#+Title: Dependently-typed tactics and certificate checking in Meta Dedukti
* Presentation
Dktactics is a Meta Dedukti implementation of a tactic typed language.
On top of this language, an untyped language of certificates is
defined and intended to be used both for interactive theorem proving
and to turn the output of automatic theorem provers into formal
proofs.
For a description of Dktactics, see the [[./manual.org][manual]].
* Dependencies
To check and compile the files, you need Dedukti v2.5.
For interactive development and conversion from certificates to
genuine proofs, Meta Dedukti v2.5 is required.
For interactive development, Meta Sukerujo is recommended.
Optionally, confluence of the [[./fol][fol]] directory can be checked by CSI^HO.
* Installation of dependencies
To install Dedukti and Meta Dedukti, clone the =meta= branch of
Dedukti git repository
#+BEGIN_SRC bash
git clone -b meta https://scm.gforge.inria.fr/anonscm/git/dedukti/dedukti.git
#+END_SRC
then compile and install the programs:
#+BEGIN_SRC bash
cd dedukti/
make
make install
#+END_SRC
To install Meta Sukerujo, clone the =skmeta= branch instead
#+BEGIN_SRC bash
git clone -b skmeta https://scm.gforge.inria.fr/anonscm/git/dedukti/dedukti.git meta_sukerujo
cd meta_sukerujo/
make
make install
#+END_SRC
CSI^HO can be downloaded from [[http://cl-informatik.uibk.ac.at/software/csi/ho/]]
* Installation of Dktactics
Invoke the =configure= script to produce the file =.config_vars=
containing the path to the dependencies.
#+BEGIN_SRC bash
./configure
#+END_SRC
Then compile all the Dedukti files
#+BEGIN_SRC bash
make
#+END_SRC
#! /bin/bash
print_to_file ()
{
echo "$1" >> .config_vars
}
print_to_stderr ()
{
echo "$1" > /dev/stderr
}
find_binary () {
# $1 is the name of the binary
# $2 is an optional extension to be used when we fallback to using
# locate
# Start by looking in path
print_to_stderr "Looking for program '$1' in PATH"
A=$(which "$1")
if [ -n "$A" ]
then
print_to_stderr "program '$1' found in PATH at \"$A\""
echo "$A"
return 0
# else use locate
else
print_to_stderr "program '$1' not found in PATH, trying with locate"
A=$(locate "$1$2" | head -n 1)
if [ -n "$A" ]
then
print_to_stderr "program '$1$2' found using locate at \"$A\""
echo "$A"
return 0
else
print_to_stderr "program '$1$2' not found"
return 1
fi
fi
}
find_and_check_binary () {
# $1 and $2 are arguments to find_binary
# $3 is the variable name
# $4 is the option to pass to the program to ask for its version
# $5 is the expected answer
A=$(find_binary $1 $2)
print_to_stderr "asking '$1' for its version number"
B=$($A $4)
print_to_stderr "'$1' has version '$B'"
if [ "$B" = "$5" ]
then
print_to_stderr "'$1' has the expected version number"
print_to_file "$3=\"$A\""
return 0
else
print_to_stderr "'$1' has version '$B' but version '$5' was expected"
return 1
fi
}
echo > .config_vars &&
# Mandatory
find_and_check_binary "dkdep" ".native" "DKDEP" "-version" "" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Dedukti v2.5" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5" &&
find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.5" &&
# Optional
find_and_check_binary "csiho" ".sh" "CSIHO" "--version" "csiho 0.3"
include ../.config_vars
ifeq ($(CSIHO),)
DKCHECK_CONFLUENCE_OPTION =
else
DKCHECK_CONFLUENCE_OPTION = -cc $(CSIHO)
endif
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
all: $(DKOS)
.PHONY: clean depend
DKCHECK_OPTIONS =
%.dko:
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) $<
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
#NAME eq.
def type := fol.type.
def types := fol.types.
def term := fol.term.
def terms := fol.terms.
def nil_term := fol.nil_term.
def cons_term := fol.cons_term.
def read_types := fol.read_types.
def prop := fol.prop.
def imp := fol.imp.
def all := fol.all.
def proof := fol.proof.
def predicate := fol.predicate.
def pred_arity := fol.pred_arity.
def pred_apply := fol.pred_apply.
def apply_pred := fol.apply_pred.
def function := fol.function.
def fun_arity := fol.fun_arity.
def fun_codomain := fol.fun_codomain.
def apply_fun := fol.apply_fun.
def O := nat.O.
def S := nat.S.
(; Equality is a family of binary predicate symbols. ;)
Eq : type -> predicate.
[A] fol.pred_arity (Eq A) --> read_types (S (S O)) A A.
def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
[A,x,y] fol.proof (fol.apply_pred (Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) -->
c : (term A -> prop) ->
proof (c x) -> proof (c y).
thm eq_refl (A : type) : proof (all A (x : term A => eq A x x))
:=
x : term A =>
c : (term A -> prop) =>
H : proof (c x) =>
H.
thm eq_symm (A : type) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A y x) (eq A x y))))
:=
x : term A =>
y : term A =>
H : proof (eq A y x) =>
H (x : term A => eq A x y) (eq_refl A y).
thm eq_trans (A : type) :
proof (all A (x : term A =>
all A (y : term A =>
all A (z : term A =>
imp (eq A x y)
(imp (eq A y z)
(eq A x z))))))
:=
x : term A =>
y : term A =>
z : term A =>
H : proof (eq A x y) =>
H2 : proof (eq A y z) =>
H2 (y : term A => eq A x y) H.
thm eq_p_equal (A : type) (p : term A -> prop) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (imp (p x) (p y)))))
:=
x : term A =>
y : term A =>
H : proof (eq A x y) =>
H p.
thm eq_f_equal (A : type) (B : type) (f : term A -> term B) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (eq B (f x) (f y)))))
:=
x : term A =>
y : term A =>
H : proof (eq A x y) =>
H (y : term A => eq B (f x) (f y)) (eq_refl B (f x)).
(; Meta theorems generalizing these two facts to any predicate or
function symbol ;)
def pred_imp : L : types -> (terms L -> prop) -> (terms L -> prop) -> prop.
[p,q] pred_imp fol.nil_type p q --> imp (p nil_term) (q nil_term)
[A,L,p,q] pred_imp (fol.cons_type A L) p q -->
all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => q (cons_term A y L l))))).
def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p p).
[p] eq_pred_imp fol.nil_type p --> Hp : proof (p nil_term) => Hp
[A,L,p] eq_pred_imp (fol.cons_type A L) p -->
x : term A =>
y : term A =>
H : proof (eq A x y) =>
H (y : term A => pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => p (cons_term A y L l))) (eq_pred_imp L (l : terms L => p (cons_term A x L l))).
thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_arity p) (apply_pred p) (apply_pred p))
:= eq_pred_imp (pred_arity p) (apply_pred p).
def fun_eq : L : types -> B : type -> (terms L -> term B) -> (terms L -> term B) -> prop.
[B,b,b'] fun_eq fol.nil_type B b b' --> eq B (b nil_term) (b' nil_term)
[A,L,B,f,f'] fun_eq (fol.cons_type A L) B f f' -->
all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f' (cons_term A y L l))))).
def eq_fun_eq : L : types -> B : type -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_type B b --> eq_refl B (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f -->
x : term A =>
y : term A =>
H : proof (eq A x y) =>
H (y : term A => fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))) (eq_fun_eq L B (l : terms L => f (cons_term A x L l))).
thm eq_fun_equal (f : function) : proof (fun_eq (fun_arity f) (fun_codomain f) (apply_fun f) (apply_fun f))
:= eq_fun_eq (fun_arity f) (fun_codomain f) (apply_fun f).
#NAME fol.
(; Polymorphic first-order logic ;)
(; Type system ;)
type : Type.
term : type -> Type.
(; Arities of function and predicate symbols are list of types ;)
types : Type.
nil_type : types.
cons_type : type -> types -> types.
(; To ease the definition of new symbols, we provide an nary
constructor read_types of list of types:
read_types n A1 A2 ... An =
cons_type A1 (cons_type A2 (... cons_type An nil_type))
;)
def nat := nat.Nat.
(; The type of the read_types function is defined inductively ;)
def read_types_T : nat -> Type.
[] read_types_T nat.O --> types.
[n] read_types_T (nat.S n) --> type -> read_types_T n.
(; Adding an element to the tail of a list of types:
snoc_type [A1 .. An] B = [A1 .. An B] ;)
def snoc_type : types -> type -> types.
[A] snoc_type nil_type A --> cons_type A nil_type
[L,A,B] snoc_type (cons_type A L) B --> cons_type A (snoc_type L B).
(; Auxiliary function:
read_tyes_acc m [A1 .. An] B1 .. Bm = [A1 .. An B1 .. Bm]
;)
def read_types_acc : n : nat -> types -> read_types_T n.
[acc] read_types_acc nat.O acc --> acc
[n,acc]
read_types_acc (nat.S n) acc
--> t : type => read_types_acc n (snoc_type acc t).
(; read_types n A1 .. An = [A1 .. An] ;)
def read_types (n : nat) : read_types_T n
:= read_types_acc n nil_type.
(; Terms are trees built from function symbols ;)
(; function is the type of function symbols, ;)
(; each time a function symbol is declared, the functions fun_arity
and fun_codomain should be extended ;)
function : Type.
def fun_arity : function -> types.
def fun_codomain : function -> type.
(; Function application is unnary ;)
terms : types -> Type.
nil_term : terms nil_type.
cons_term : A : type -> term A ->
tail_types : types ->
terms tail_types ->
terms (cons_type A tail_types).
def apply_fun : f : function ->
terms (fun_arity f) ->
term (fun_codomain f).
(; To limit the number of parentheses when writing function
applications, we derive an nary application fun_apply ;)
(; read_f_T [A1 .. An] C --> A1 -> .. -> An -> C ;)
def read_f_T : types -> type -> Type.
[C] read_f_T nil_type C --> term C
[A,As,C] read_f_T (cons_type A As) C --> term A -> read_f_T As C.
(; read_f [A1 .. An] C f a1 .. an --> f [a1 .. an] ;)
def read_f : As : types -> C : type -> (terms As -> term C) -> read_f_T As C.
[C,f] read_f nil_type C f --> f nil_term.
[A,As,C,f] read_f (cons_type A As) C f --> a : term A => read_f As C (as : terms As => f (cons_term A a As as)).
def fun_apply (f : function) := read_f (fun_arity f) (fun_codomain f) (apply_fun f).
(; Formulae ;)
prop : Type.
(; Connectives ;)
false : prop.
and : prop -> prop -> prop.
or : prop -> prop -> prop.
imp : prop -> prop -> prop.
all : A : type -> (term A -> prop) -> prop.
ex : A : type -> (term A -> prop) -> prop.
(; Derived connectives ;)
def not (p : prop) := imp p false.
def true := not false.
def eqv (p : prop) (q : prop) := and (imp p q) (imp q p).
(; Predicate application is also nary ;)
predicate : Type.
def pred_arity : predicate -> types.
def apply_pred : p : predicate ->
terms (pred_arity p) ->
prop.
(; To limit the number of parentheses when writing predicate
applications, we derive an nary application pred_apply ;)
(; read_p_T [A1 .. An] --> A1 -> .. -> prop ;)
def read_p_T : types -> Type.
[] read_p_T nil_type --> prop
[A,As] read_p_T (cons_type A As) --> term A -> read_p_T As.
(; read_p [A1 .. An] p a1 .. an --> p [a1 .. an] ;)
def read_p : As : types -> (terms As -> prop) -> read_p_T As.
[p] read_p nil_type p --> p nil_term.
[A,As,p] read_p (cons_type A As) p -->
a : term A => read_p As (as : terms As => p (cons_term A a As as)).
def pred_apply (p : predicate) := read_p (pred_arity p) (apply_pred p).
(; The type of proofs of a formula is defined using an impredicative encoding ;)
def proof : prop -> Type.
[] proof false -->
c : prop -> proof c
[a,b] proof (and a b) -->
c : prop ->
(proof a -> proof b -> proof c) ->
proof c
[a,b] proof (or a b) -->
c : prop ->
(proof a -> proof c) ->
(proof b -> proof c) ->
proof c
[a,b] proof (imp a b) -->
proof a -> proof b
[A,p] proof (all A p) -->
a : term A -> proof (p a)
[A,p] proof (ex A p) -->
c : prop ->
(a : term A -> proof (p a) -> proof c) ->
proof c.
(; Natural deduction ;)
thm false_elim (a : prop) : proof false -> proof a :=
H : proof false => H a.
thm true_intro : proof true :=
H : proof false => H.
thm and_intro (a : prop) (b : prop) : proof a -> proof b -> proof (and a b) :=
Ha : proof a =>
Hb : proof b =>
c : prop =>
Hc : (proof a -> proof b -> proof c) =>
Hc Ha Hb.
thm and_elim_1 (a : prop) (b : prop) : proof (and a b) -> proof a :=
Hab : proof (and a b) =>
Hab a (Ha : proof a => Hb : proof b => Ha).
thm and_elim_2 (a : prop) (b : prop) : proof (and a b) -> proof b :=
Hab : proof (and a b) =>
Hab b (Ha : proof a => Hb : proof b => Hb).
thm or_intro_1 (a : prop) (b : prop) : proof a -> proof (or a b) :=
Ha : proof a =>
c : prop =>
Hac : (proof a -> proof c) =>
Hbc : (proof b -> proof c) =>
Hac Ha.
thm or_intro_2 (a : prop) (b : prop) : proof b -> proof (or a b) :=
Hb : proof b =>
c : prop =>
Hac : (proof a -> proof c) =>
Hbc : (proof b -> proof c) =>
Hbc Hb.
thm or_elim (a : prop) (b : prop) (c : prop) : proof (or a b) -> (proof a -> proof c) -> (proof b -> proof c) -> proof c :=
Hab : proof (or a b) => Hab c.
thm imp_intro (a : prop) (b : prop) : (proof a -> proof b) -> proof (imp a b) :=
Hab : (proof a -> proof b) => Hab.
thm imp_elim (a : prop) (b : prop) : proof (imp a b) -> proof a -> proof b :=
Hab : proof (imp a b) => Hab.
thm all_intro (A : type) (p : term A -> prop) :
(a : term A -> proof (p a)) -> proof (all A p)
:=
HAp : (a : term A -> proof (p a)) => HAp.
thm all_elim (A : type) (p : term A -> prop) :
proof (all A p) -> a : term A -> proof (p a)
:=
HAp : proof (all A p) => HAp.
thm ex_intro (A : type) (p : term A -> prop) :
a : term A -> proof (p a) -> proof (ex A p)
:=
a : term A =>
Hpa : proof (p a) =>
c : prop =>
Hc : (x : term A -> proof (p x) -> proof c) =>
Hc a Hpa.
thm ex_elim (A : type) (p : term A -> prop) (c : prop) :
proof (ex A p) ->
(a : term A -> proof (p a) -> proof c) ->
proof c
:=
HAp : proof (ex A p) => HAp c.
#NAME nat.
Nat : Type.
O : Nat.
S : Nat -> Nat.
#NAME presburger.
(; The first-order theory of Presburger arithmetic:
https://en.wikipedia.org/wiki/Presburger_arithmetic ;)
(; There is just one sort representing natural numbers ;)
Nat : fol.type.
(; There is just one predicate symbol for equality ;)
EQ : fol.predicate.
(; Function symbols:
- 0 : Nat.
- 1 : Nat.
- + : [Nat, Nat] -> Nat.
;)
ZERO : fol.function.
ONE : fol.function.
ADD : fol.function.
(; Arities ;)
[] fol.pred_arity EQ --> fol.read_types (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_arity ZERO --> fol.nil_type.
[] fol.fun_arity ONE --> fol.nil_type.
[] fol.fun_arity ADD --> fol.read_types (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_codomain ZERO --> Nat.
[] fol.fun_codomain ONE --> Nat.
[] fol.fun_codomain ADD --> Nat.
(; Abbreviations ;)
def eq := fol.pred_apply EQ.
def 0 := fol.fun_apply ZERO.
def 1 := fol.fun_apply ONE.
def add := fol.fun_apply ADD.
def succ (x : fol.term Nat) := add x 1.
(; Axioms ;)
(; 0 != x + 1 ;)
P1 : fol.proof (fol.all Nat (x => fol.not (eq 0 (succ x)))).
(; x+1 = y+1 -> x = y ;)
P2 : fol.proof (fol.all Nat (x => fol.all Nat (y => fol.imp (eq (succ x) (succ y)) (eq x y)))).
(; x+0 = x ;)
P3 : fol.proof (fol.all Nat (x => eq (add x 0) x)).
(; x + (y + 1) = (x + y) + 1 ;)
P4 : fol.proof (fol.all Nat (x => fol.all Nat (y => eq (add x (succ y)) (succ (add x y))))).
(; Axiom schema of induction ;)
P5 : p : (fol.term Nat -> fol.prop) ->
fol.proof (fol.imp (fol.and (p 0) (fol.all Nat (x => fol.imp (p x) (p (succ x))))) (fol.all Nat p)).
\ No newline at end of file
This diff is collapsed.
include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
FOLDKS = $(wildcard ../fol/*.dk)
DKOS = $(DKS:.dk=.dko)
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
all: $(DKOS)
.PHONY: clean depend
DKCHECK_OPTIONS = -I ../fol -nl
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
This diff is collapsed.
#NAME eqcert.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
(setq-local dedukti-check-options '("-nc" "-nl" "-I" "../fol"))
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; Certificates for manipulating equalities ;)
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
not_an_equality : tac.exc.
def match_equality : prop -> (A : type -> term A -> term A -> certificate) -> certificate -> certificate.
[c] match_equality fol.false _ c --> c
[c] match_equality (fol.and _ _) _ c --> c
[c] match_equality (fol.or _ _) _ c --> c
[c] match_equality (fol.imp _ _) _ c --> c
[c] match_equality (fol.all _ _) _ c --> c
[c] match_equality (fol.ex _ _) _ c --> c
[c,A,a,b]
match_equality (fol.apply_pred
(eq.Eq A)
(fol.cons_term _ a
_ (fol.cons_term _ b
_ fol.nil_term)))
c _
--> c A a b
[c] match_equality (fol.apply_pred _ _) _ c --> c.
not_convertible : A : type -> term A -> term A -> tac.exc.
(; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate :=
cert.with_goal (G =>
match_equality G (A : type => a : term A => b : term A =>
cert.try (cert.exact (eq.eq A a a) (eq.eq_refl A a))
(__ => cert.raise (not_convertible A a b))
)
(cert.raise not_an_equality)).
(; symmetry c proves a = b if c proves b = a ;)
def symmetry (c : certificate) : certificate :=
cert.with_goal (G =>
match_equality G (A : type => a : term A => b : term A =>
cert.refine (eq.eq A b a)
(eq.eq A a b)
(eq.eq_symm A a b)
c
)
(cert.raise not_an_equality)).
trans_bad_type : tac.exc.
(; transitivity A b c1 c2 proves a = c if c1 proves a = b and c2 proves b = c ;)
def transitivity (A : type) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
cert.with_goal (G =>
match_equality G (A' : type => a : term A' => c : term A' =>
cert.ifeq_type A A' (f =>
cert.refine2 (eq.eq A' a (f b))
(eq.eq A' (f b) c)
(eq.eq A' a c)
(eq.eq_trans A' a (f b) c)
c1
c2)
(cert.raise trans_bad_type))
(cert.raise not_an_equality)).
(; f_equal f c .. cn proves f(a1, .., an) = f(b1, .., bn) if each ci proves ai = bi ;)
def match_f_equal_goal : prop ->
(f : fol.function ->
fol.terms (fol.fun_arity f) ->
fol.terms (fol.fun_arity f) ->
certificate) ->
certificate.
[A,f,as,bs,c] match_f_equal_goal (fol.apply_pred
(eq.Eq A)
(fol.cons_term _ (fol.apply_fun f as)
_ (fol.cons_term _ (fol.apply_fun f bs)
_ fol.nil_term)))
c
--> c f as bs.
certificates : fol.types -> Type.
nil_cert : certificates fol.nil_type.
cons_cert : A : type -> As : fol.types -> certificate -> certificates As -> certificates (fol.cons_type A As).
def ifeq_certs : L : fol.types ->
L' : fol.types ->
certificates L ->
certificates L'.
[L,c] ifeq_certs L L c --> c.
(; f_equal_fun L B f [a1 .. an] [b1 .. bn] [c1 .. cn] proves
f [a1 .. an] = f [b1 .. bn] if each ci proves ai = bi ;)
def f_equal_fun : L : fol.types ->
B : type ->
(fol.terms L -> term B) ->
fol.terms L ->
fol.terms L ->
certificates L -> certificate.
[] f_equal_fun _ _ _ fol.nil_term fol.nil_term nil_cert --> reflexivity
[B,f,A,a,As,as,b,bs,c,cs]
f_equal_fun
(fol.cons_type _ _)
B
f
(fol.cons_term A a As as)
(fol.cons_term _ b _ bs)
(cons_cert _ _ c cs)
-->
cert.refine2
(eq.eq A a b)
(eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs)))
(eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
(Hab : proof (eq.eq A a b) =>
Hf : proof (eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs))) =>
Hab (b => eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
Hf)
c
(f_equal_fun As B (l => f (fol.cons_term A a As l)) as bs cs).
def f_equal_fun_on_goal (L : fol.types) (cs : certificates L) : certificate
:=
cert.with_goal (G => match_f_equal_goal G
(f => as => bs =>
f_equal_fun
(fol.fun_arity f)
(fol.fun_codomain f)
(fol.apply_fun f)
as bs (ifeq_certs L (fol.fun_arity f) cs)
)).
def f_equal_T : fol.types -> Type.
[] f_equal_T fol.nil_type --> certificate
[As] f_equal_T (fol.cons_type _ As) --> certificate -> f_equal_T As.
def append_type : fol.types -> fol.types -> fol.types.
[As] append_type As fol.nil_type --> As
[As,B,Bs]
append_type As (fol.cons_type B Bs) -->
append_type (fol.snoc_type As B) Bs.
def snoc_cert : L : fol.types ->
A : type ->
certificates L ->