eqcert.dk 3.46 KB
Newer Older
Raphael Cauderlier's avatar
Raphael Cauderlier committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
#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 term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.

not_an_equality : tac.exc.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
18
def match_equality : prop -> (A : Type -> term A -> term A -> certificate) -> certificate -> certificate.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35

[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.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
36
not_convertible : A : Type -> term A -> term A -> tac.exc.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
37 38 39 40

(; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate :=
 cert.with_goal (G =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
41
            match_equality G (A : Type => a : term A => b : term A =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
42 43 44 45 46 47 48 49
                             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 =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
50
             match_equality G (A : Type => a : term A => b : term A =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
51 52 53 54 55 56 57 58 59
                               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 ;)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
60
def transitivity (A : Type) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
61
  cert.with_goal (G =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
62
             match_equality G (A' : Type => a : term A' => c : term A' =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
63 64 65 66 67 68 69 70 71 72 73
                               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)).

(; rewrite A a b c1 c2 proves G if c1 proves a = b and c2 proves G{b/a} ;)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
74
def rewrite (A : Type) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate
Raphael Cauderlier's avatar
Raphael Cauderlier committed
75 76 77 78 79 80 81 82 83 84 85
:=
  cert.with_goal (G =>
             cert.refine2 (eq.eq A a b)
                     (unif.subst_prop (unif.cons_subst A b a unif.empty_subst) G)
                     G
                       (Hab : proof (eq.eq A a b) =>
                        Hab (a =>
                             unif.subst_prop
                               (unif.cons_subst A b a unif.empty_subst) G))
                       c1
                       c2).