Commit 701fcb23 authored by Raphael Cauderlier's avatar Raphael Cauderlier

certificate -> tactic

parent f41aedef
......@@ -30,27 +30,26 @@ def drinker_statement : fol.prop :=
def ndrink (x : fol.term BAR) := fol.not (drink x).
def drinker_paradox : fol.proof drinker_statement :=
mtac.mrun drinker_statement (
cert.run drinker_statement cert.nil_ctx
(classical_cert.prop_case (fol.all BAR drink)
tactic.prove drinker_statement
(classical_tactics.prop_case (fol.all BAR drink)
(; ∀ ⊢ ∃x. drink x → ∀ ;)
(cert.exists BAR Joe (cert.intro cert.assumption))
(tactic.exists BAR Joe (tactic.intro tactic.assumption))
(; ¬∀ ⊢ ∃x. drink x → ∀ ;)
(cert.destruct_imp
(tactic.destruct_imp
(fol.not (fol.all BAR drink))
(fol.ex BAR ndrink)
(; ¬∀ ⊢ ¬∀ → ∃¬ ;)
(cert.exact
(tactic.exact
(fol.imp (fol.not (fol.all BAR drink))
(fol.ex BAR ndrink))
(classical_cert.not_all_is_ex_not BAR drink))
(classical_tactics.not_all_is_ex_not BAR drink))
(; ¬∀ ⊢ ¬∀ ;)
cert.assumption
tactic.assumption
(; ¬∀, ∃¬ ⊢ ∃x. drink x → ∀ ;)
(cert.with_assumption (E => e =>
cert.destruct_ex BAR ndrink (cert.exact E e)
(tactic.with_assumption (E => e =>
tactic.destruct_ex BAR ndrink (tactic.exact E e)
(; ¬∀, ∃¬, John, ¬drink John ⊢ ∃x. drink x → ∀ ;)
(cert.with_variable (B : fol.sort => John : fol.term B =>
cert.exists B John
(tactic.with_variable (B : fol.sort => John : fol.term B =>
tactic.exists B John
(; ¬∀, ∃¬, John, ¬drink John ⊢ drink John → ∀ ;)
(cert.intro cert.absurd)))))))).
(tactic.intro tactic.absurd))))))).
#NAME inhabited_sorts.
def default_value : A : fol.sort -> fol.term A.
This diff is collapsed.
#NAME classical_cert.
#NAME classical_tactics.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
......@@ -7,14 +7,14 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; Classical theorems and certificate combinators ;)
(; Classical theorems and tacticals ;)
(; Reason by case on a the truth of a formula (using excluded middle) ;)
def prop_case (P : fol.prop) :
cert.certificate -> cert.certificate -> cert.certificate
tactic.tactic -> tactic.tactic -> tactic.tactic
:=
cert.destruct_or P (fol.not P)
(cert.exact
tactic.destruct_or P (fol.not P)
(tactic.exact
(fol.or P (fol.not P))
(classical.excluded_middle P)).
......@@ -23,91 +23,88 @@ def prop_case (P : fol.prop) :
cannot quantify over formulae ;)
def nnpp (P : fol.prop) : fol.proof (fol.imp (fol.not (fol.not P)) P)
:=
cert.cert_run (fol.imp (fol.not (fol.not P)) P)
(cert.intro
tactic.prove (fol.imp (fol.not (fol.not P)) P)
(tactic.intro
(; ¬¬P ⊢ P ;)
(prop_case P
(; ¬¬P, P ⊢ P ;)
cert.assumption
tactic.assumption
(; ¬¬P, ¬P ⊢ P ;)
cert.absurd)).
tactic.absurd)).
(; Use double-negation elimination to do a proof by contradiction.
(contradict c) proves Γ ⊢ P if c proves Γ, ¬P ⊢ ⊥ ;)
def contradict (c : cert.certificate) : cert.certificate :=
cert.with_goal
def contradict (c : tactic.tactic) : tactic.tactic :=
tactic.with_goal
(P =>
cert.refine
tactic.refine
(fol.not (fol.not P))
P
(fol.imp_elim (fol.not (fol.not P)) P (nnpp P))
(cert.intro c)).
(tactic.intro c)).
(; De Morgan laws ;)
def not_and_is_or_not (A : fol.prop) (B : fol.prop) :
fol.proof (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))
:=
cert.cert_run (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))
(cert.intro
tactic.prove (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))
(tactic.intro
(; ¬∧ ⊢ ∨¬ ;)
(contradict
(; ¬∧, ¬∨¬ ⊢ ⊥;)
(cert.destruct_imp
(tactic.destruct_imp
(fol.and A B)
fol.false
(; ¬∧, ¬∨¬ ⊢ ¬∧ ;)
cert.assumption
tactic.assumption
(; ¬∧, ¬∨¬ ⊢ ∧ ;)
(cert.split
(tactic.split
(; ¬∧, ¬∨¬ ⊢ A ;)
(contradict
(; ¬∧, ¬∨¬, ¬A ⊢ ⊥ ;)
(cert.destruct_imp
(tactic.destruct_imp
(fol.or (fol.not A) (fol.not B))
fol.false
(; ¬∧, ¬∨¬, ¬A ⊢ ¬∨¬ ;)
cert.assumption
tactic.assumption
(; ¬∧, ¬∨¬, ¬A ⊢ ∨¬ ;)
(cert.left cert.assumption)
(tactic.left tactic.assumption)
(; ¬∧, ¬∨¬, ¬A, ⊥ ⊢ ⊥ ;)
cert.assumption))
tactic.assumption))
(; ¬∧, ¬∨¬ ⊢ B ;)
(contradict
(cert.destruct_imp
(tactic.destruct_imp
(fol.or (fol.not A) (fol.not B))
fol.false
cert.assumption
(cert.right cert.assumption)
cert.assumption)))
tactic.assumption
(tactic.right tactic.assumption)
tactic.assumption)))
(; ¬∧, ¬∨¬, ⊥ ⊢ ⊥ ;)
cert.assumption))).
tactic.assumption))).
(; Same for quantifiers ;)
def not_all_is_ex_not (A : fol.sort) (P : fol.term A -> fol.prop) :
fol.proof (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
:=
mtac.mrun (fol.imp (fol.not (fol.all A (x => P x)))
tactic.prove (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
(cert.run (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
cert.nil_ctx
(cert.intro
(; ¬∀ ⊢ ∃¬ ;)
(contradict
(; ¬∀, ¬∃¬ ⊢ ⊥ ;)
(cert.destruct_imp (fol.all A (x => P x)) fol.false
cert.assumption
(cert.intro
(; ¬∀, ¬∃¬, x ⊢ P x ;)
(contradict
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ⊥ ;)
(cert.destruct_imp
(fol.ex A (x => fol.not (P x)))
fol.false
cert.assumption
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ∃¬ ;)
(cert.with_variable
(A => a => cert.exists A a cert.assumption))
cert.assumption)))
cert.assumption)))).
(tactic.intro
(; ¬∀ ⊢ ∃¬ ;)
(contradict
(; ¬∀, ¬∃¬ ⊢ ⊥ ;)
(tactic.destruct_imp (fol.all A (x => P x)) fol.false
tactic.assumption
(tactic.intro
(; ¬∀, ¬∃¬, x ⊢ P x ;)
(contradict
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ⊥ ;)
(tactic.destruct_imp
(fol.ex A (x => fol.not (P x)))
fol.false
tactic.assumption
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ∃¬ ;)
(tactic.with_variable
(A => a => tactic.exists A a tactic.assumption))
tactic.assumption)))
tactic.assumption))).
#NAME eqcert.
#NAME eqtac.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
......@@ -7,19 +7,19 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; Certificates for manipulating equalities ;)
(; Tactics for manipulating equalities ;)
def sort := fol.sort.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
def tactic := tactic.tactic.
def eq := eq.eq.
def imp := fol.imp.
def all := fol.all.
not_an_equality : mtac.exc.
def match_equality : prop -> (A : sort -> term A -> term A -> certificate) -> certificate -> certificate.
def match_equality : prop -> (A : sort -> term A -> term A -> tactic) -> tactic -> tactic.
[c] match_equality fol.false _ c --> c
[c] match_equality (fol.and _ _) _ c --> c
......@@ -40,34 +40,34 @@ def match_equality : prop -> (A : sort -> term A -> term A -> certificate) -> ce
not_convertible : A : sort -> term A -> term A -> mtac.exc.
(; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate :=
cert.with_goal (G =>
def reflexivity : tactic :=
tactic.with_goal (G =>
match_equality G (A : sort => a : term A => b : term A =>
cert.try (cert.exact (eq A a a) (fol.all_elim A (x => eq A x x) (eq.eq_refl A) a))
(__ => cert.raise (not_convertible A a b))
tactic.try (tactic.exact (eq A a a) (fol.all_elim A (x => eq A x x) (eq.eq_refl A) a))
(__ => tactic.raise (not_convertible A a b))
)
(cert.raise not_an_equality)).
(tactic.raise not_an_equality)).
(; symmetry c proves a = b if c proves b = a ;)
def symmetry (c : certificate) : certificate :=
cert.with_goal (G =>
def symmetry (c : tactic) : tactic :=
tactic.with_goal (G =>
match_equality G (A : sort => a : term A => b : term A =>
cert.refine (eq A b a)
tactic.refine (eq A b a)
(eq A a b)
(fol.imp_elim (eq A b a) (eq A a b)
(fol.all_elim A (y => imp (eq A y a) (eq A a y))
(fol.all_elim A (x => all A (y => imp (eq A y x) (eq A x y))) (eq.eq_symm A) a) b))
c
)
(cert.raise not_an_equality)).
(tactic.raise not_an_equality)).
trans_bad_type : mtac.exc.
(; transitivity A b c1 c2 proves a = c if c1 proves a = b and c2 proves b = c ;)
def transitivity (A : sort) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
cert.with_goal (G =>
def transitivity (A : sort) (b : term A) (c1 : tactic) (c2 : tactic) : tactic :=
tactic.with_goal (G =>
match_equality G (A' : sort => a : term A' => c : term A' =>
cert.ifeq_sort A A' (f =>
cert.refine2 (eq A' a (f b))
tactic.ifeq_sort A A' (f =>
tactic.refine2 (eq A' a (f b))
(eq A' (f b) c)
(eq A' a c)
(H1 => H2 =>
......@@ -79,8 +79,8 @@ def transitivity (A : sort) (b : term A) (c1 : certificate) (c2 : certificate) :
(eq.eq_trans A') a) (f b)) c) H1) H2)
c1
c2)
(cert.raise trans_bad_type))
(cert.raise not_an_equality)).
(tactic.raise trans_bad_type))
(tactic.raise not_an_equality)).
(; f_equal f c .. cn proves f(a1, .., an) = f(b1, .., bn) if each ci proves ai = bi ;)
......@@ -88,8 +88,8 @@ def match_f_equal_goal : prop ->
(f : fol.function ->
fol.terms (fol.fun_domain f) ->
fol.terms (fol.fun_domain f) ->
certificate) ->
certificate.
tactic) ->
tactic.
[A,f,as,bs,c] match_f_equal_goal (fol.apply_pred
(eq.Eq A)
(fol.cons_term _ (fol.apply_fun f as)
......@@ -100,7 +100,7 @@ def match_f_equal_goal : prop ->
certificates : fol.sorts -> Type.
nil_cert : certificates fol.nil_sort.
cons_cert : A : sort -> As : fol.sorts -> certificate -> certificates As -> certificates (fol.cons_sort A As).
cons_cert : A : sort -> As : fol.sorts -> tactic -> certificates As -> certificates (fol.cons_sort A As).
def ifeq_certs : L : fol.sorts ->
L' : fol.sorts ->
......@@ -115,7 +115,7 @@ def f_equal_fun : L : fol.sorts ->
(fol.terms L -> term B) ->
fol.terms L ->
fol.terms L ->
certificates L -> certificate.
certificates L -> tactic.
[] 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
......@@ -126,7 +126,7 @@ def f_equal_fun : L : fol.sorts ->
(fol.cons_term _ b _ bs)
(cons_cert _ _ c cs)
-->
cert.refine2
tactic.refine2
(eq A a b)
(eq B
(f (fol.cons_term A a As as))
......@@ -145,9 +145,9 @@ def f_equal_fun : L : fol.sorts ->
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.sorts) (cs : certificates L) : certificate
def f_equal_fun_on_goal (L : fol.sorts) (cs : certificates L) : tactic
:=
cert.with_goal (G => match_f_equal_goal G
tactic.with_goal (G => match_f_equal_goal G
(f => as => bs =>
f_equal_fun
(fol.fun_domain f)
......@@ -157,8 +157,8 @@ def f_equal_fun_on_goal (L : fol.sorts) (cs : certificates L) : certificate
)).
def f_equal_T : fol.sorts -> Type.
[] f_equal_T fol.nil_sort --> certificate
[As] f_equal_T (fol.cons_sort _ As) --> certificate -> f_equal_T As.
[] f_equal_T fol.nil_sort --> tactic
[As] f_equal_T (fol.cons_sort _ As) --> tactic -> f_equal_T As.
def append_type : fol.sorts -> fol.sorts -> fol.sorts.
[As] append_type As fol.nil_sort --> As
......@@ -169,7 +169,7 @@ def append_type : fol.sorts -> fol.sorts -> fol.sorts.
def snoc_cert : L : fol.sorts ->
A : sort ->
certificates L ->
certificate ->
tactic ->
certificates (fol.snoc_sort L A).
[A,c] snoc_cert _ A nil_cert c --> cons_cert A fol.nil_sort c nil_cert
[A,B,Bs,c,cs,ca]
......@@ -189,7 +189,7 @@ def f_equal_fun_n : L' : fol.sorts ->
[A,As,L,B,f,as,bs,cs]
f_equal_fun_n (fol.cons_sort A As) L cs
-->
c : certificate =>
c : tactic =>
f_equal_fun_n As (fol.snoc_sort L A) (snoc_cert L A cs c).
def f_equal (f : fol.function) :=
......@@ -199,10 +199,10 @@ def f_equal (f : fol.function) :=
nil_cert.
(; rewrite A a b c1 c2 proves G if c1 proves a = b and c2 proves G{b/a} ;)
def rewrite (A : sort) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate
def rewrite (A : sort) (a : term A) (b : term A) (c1 : tactic) (c2 : tactic) : tactic
:=
cert.with_goal (G =>
cert.refine2 (eq A a b)
tactic.with_goal (G =>
tactic.refine2 (eq A a b)
(unif.subst_prop (unif.cons_subst A b a unif.empty_subst) G)
G
(Hab : proof (eq A a b) =>
......
......@@ -34,7 +34,7 @@ def or := fol.or.
def all := fol.all.
def sort := fol.sort.
def term := fol.term.
def certificate := cert.certificate.
def tactic := tactic.tactic.
def substitution := unif.substitution.
def nat := nat.Nat.
......
This diff is collapsed.
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