Commit 8a335c4f authored by Raphael Cauderlier's avatar Raphael Cauderlier

Remove dependency on the impredicative definition of equality

parent 5db203c6
......@@ -33,62 +33,64 @@ Eq : type -> predicate.
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).
(; [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.
def 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) :
def eq_congr : A : type -> x : term A -> y : term A -> proof (eq A x y) -> c : (term A -> prop) -> proof (c x) -> proof (c y).
def 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) :
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). ;)
def 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) :
(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. ;)
def 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) :
imp (eq A x y) (imp (p x) (p y))))).
(; := ;)
(; x : term A => ;)
(; y : term A => ;)
(; H : proof (eq A x y) => ;)
(; H p. ;)
def 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)).
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 ;)
......@@ -106,7 +108,7 @@ def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p 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))).
eq_congr 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).
......@@ -124,7 +126,7 @@ def eq_fun_eq : L : types -> B : type -> f : (terms L -> term B) -> proof (fun_e
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))).
eq_congr 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).
......@@ -127,7 +127,7 @@ def f_equal_fun : L : fol.types ->
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
eq.eq_congr A a b Hab (b => eq.eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
Hf)
......@@ -195,7 +195,7 @@ def rewrite (A : type) (a : term A) (b : term A) (c1 : certificate) (c2 : certif
(unif.subst_prop (unif.cons_subst A b a unif.empty_subst) G)
G
(Hab : proof (eq.eq A a b) =>
Hab (a =>
eq.eq_congr A a b Hab (a =>
unif.subst_prop
(unif.cons_subst A b a unif.empty_subst) G))
c1
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment