eqcert.dk

#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 sort := fol.sort.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
def eq := eq.eq.
def imp := fol.imp.
def all := fol.all.

not_an_equality : tac.exc.
def match_equality : prop -> (A : sort -> 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 : sort -> 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 : 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))
                             )
                             (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 : sort => a : term A => b : term A =>
                               cert.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)).

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 : sort) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
  cert.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))
                                       (eq A' (f b) c)
                                       (eq A' a c)
                                       (H1 => H2 =>
                                        fol.imp_elim (eq A' (f b) c) (eq A' a c)
                                          (fol.imp_elim (eq A' a (f b)) (imp (eq A' (f b) c) (eq A' a c))
                                            (fol.all_elim A' (z => imp (eq A' a (f b)) (imp (eq A' (f b) z) (eq A' a z)))
                                              (fol.all_elim A' (y => all A' (z => imp (eq A' a y) (imp (eq A' y z) (eq A' a z))))
                                                (fol.all_elim A' (x => all A' (y => all A' (z => imp (eq A' x y) (imp (eq A' y z) (eq A' x z)))))
                                                  (eq.eq_trans A') a) (f b)) c) H1) H2)
                                       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.sorts -> Type.
nil_cert : certificates fol.nil_sort.
cons_cert : A : sort -> As : fol.sorts -> certificate -> certificates As -> certificates (fol.cons_sort A As).

def ifeq_certs : L : fol.sorts ->
                 L' : fol.sorts ->
                 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.sorts ->
                  B : sort ->
                  (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_sort _ _)
      B
      f
      (fol.cons_term A a As as)
      (fol.cons_term _ b _ bs)
      (cons_cert _ _ c cs)
   -->
   cert.refine2
     (eq A a b)
     (eq B
        (f (fol.cons_term A a As as))
        (f (fol.cons_term A a As bs)))
     (eq B
        (f (fol.cons_term A a As as))
        (f (fol.cons_term A b As bs)))
     (Hab : proof (eq A a b) =>
      Hf : proof (eq B
                    (f (fol.cons_term A a As as))
                    (f (fol.cons_term A a As bs))) =>
      eq.eq_congr A a b Hab (b => 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.sorts) (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.sorts -> Type.
[] f_equal_T fol.nil_sort --> certificate
[As] f_equal_T (fol.cons_sort _ As) --> certificate -> f_equal_T As.

def append_type : fol.sorts -> fol.sorts -> fol.sorts.
[As] append_type As fol.nil_sort --> As
[As,B,Bs]
    append_type As (fol.cons_sort B Bs) -->
    append_type (fol.snoc_sort As B) Bs.

def snoc_cert : L : fol.sorts ->
                A : sort ->
                certificates L ->
                certificate ->
                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]
    snoc_cert (fol.cons_sort _ _) A (cons_cert B Bs c cs) ca
      -->
    cons_cert B (fol.snoc_sort Bs A) c (snoc_cert Bs A cs ca).


def f_equal_fun_n : L' : fol.sorts ->
                    L : fol.sorts ->
                    certificates L ->
                    f_equal_T L'.
[L,B,f,as,bs,cs]
    f_equal_fun_n fol.nil_sort L cs
      -->
    f_equal_fun_on_goal L cs
[A,As,L,B,f,as,bs,cs]
    f_equal_fun_n (fol.cons_sort A As) L cs
      -->
    c : certificate =>
    f_equal_fun_n As (fol.snoc_sort L A) (snoc_cert L A cs c).

def f_equal (f : fol.function) :=
  f_equal_fun_n
    (fol.fun_arity f)
    fol.nil_sort
    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
:=
  cert.with_goal (G =>
             cert.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) =>
                        eq.eq_congr A a b Hab (a =>
                             unif.subst_prop
                               (unif.cons_subst A b a unif.empty_subst) G))
                       c1
                       c2).