eqcert.dk 8.19 KB
Newer Older
Raphael Cauderlier's avatar
Raphael Cauderlier committed
1 2 3 4 5 6 7 8 9 10 11
#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 ;)

Raphael Cauderlier's avatar
Raphael Cauderlier committed
12
def sort := fol.sort.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
13 14 15 16
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
17 18 19
def eq := eq.eq.
def imp := fol.imp.
def all := fol.all.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
20 21

not_an_equality : tac.exc.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
22
def match_equality : prop -> (A : sort -> term A -> term A -> certificate) -> certificate -> certificate.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

[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
40
not_convertible : A : sort -> term A -> term A -> tac.exc.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
41 42 43 44

(; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate :=
 cert.with_goal (G =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
45
            match_equality G (A : sort => a : term A => b : term A =>
46
                             cert.try (cert.exact (eq A a a) (fol.all_elim A (x => eq A x x) (eq.eq_refl A) a))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
47 48 49 50 51 52 53
                                 (__ => 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
54
             match_equality G (A : sort => a : term A => b : term A =>
55 56 57 58 59
                               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))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
60 61 62 63 64 65
                                      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
66
def transitivity (A : sort) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
67
  cert.with_goal (G =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
68 69
             match_equality G (A' : sort => a : term A' => c : term A' =>
                               cert.ifeq_sort A A' (f =>
70 71 72 73 74 75 76 77 78 79
                               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)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
80 81 82 83 84
                                       c1
                                       c2)
                              (cert.raise trans_bad_type))
                              (cert.raise not_an_equality)).

85 86 87 88
(; 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 ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
89 90
                          fol.terms (fol.fun_domain f) ->
                          fol.terms (fol.fun_domain f) ->
91 92 93 94 95 96 97 98 99 100
                          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.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
101 102 103
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).
104

Raphael Cauderlier's avatar
Raphael Cauderlier committed
105 106
def ifeq_certs : L : fol.sorts ->
                 L' : fol.sorts ->
107 108 109 110 111 112
                 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 ;)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
113 114
def f_equal_fun : L : fol.sorts ->
                  B : sort ->
115 116 117 118 119 120 121
                  (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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
122
      (fol.cons_sort _ _)
123 124 125 126 127 128 129
      B
      f
      (fol.cons_term A a As as)
      (fol.cons_term _ b _ bs)
      (cons_cert _ _ c cs)
   -->
   cert.refine2
130 131
     (eq A a b)
     (eq B
132 133
        (f (fol.cons_term A a As as))
        (f (fol.cons_term A a As bs)))
134
     (eq B
135 136
        (f (fol.cons_term A a As as))
        (f (fol.cons_term A b As bs)))
137 138
     (Hab : proof (eq A a b) =>
      Hf : proof (eq B
139 140
                    (f (fol.cons_term A a As as))
                    (f (fol.cons_term A a As bs))) =>
141
      eq.eq_congr A a b Hab (b => eq B
142 143 144 145 146 147
                  (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).

Raphael Cauderlier's avatar
Raphael Cauderlier committed
148
def f_equal_fun_on_goal (L : fol.sorts) (cs : certificates L) : certificate
149 150 151 152
 :=
   cert.with_goal (G => match_f_equal_goal G
                  (f => as => bs =>
                   f_equal_fun
Raphael Cauderlier's avatar
Raphael Cauderlier committed
153
                     (fol.fun_domain f)
154 155
                     (fol.fun_codomain f)
                     (fol.apply_fun f)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
156
                     as bs (ifeq_certs L (fol.fun_domain f) cs)
157 158
                  )).

Raphael Cauderlier's avatar
Raphael Cauderlier committed
159 160 161
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.
162

Raphael Cauderlier's avatar
Raphael Cauderlier committed
163 164
def append_type : fol.sorts -> fol.sorts -> fol.sorts.
[As] append_type As fol.nil_sort --> As
165
[As,B,Bs]
Raphael Cauderlier's avatar
Raphael Cauderlier committed
166 167
    append_type As (fol.cons_sort B Bs) -->
    append_type (fol.snoc_sort As B) Bs.
168

Raphael Cauderlier's avatar
Raphael Cauderlier committed
169 170
def snoc_cert : L : fol.sorts ->
                A : sort ->
171 172
                certificates L ->
                certificate ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
173 174
                certificates (fol.snoc_sort L A).
[A,c] snoc_cert _ A nil_cert c --> cons_cert A fol.nil_sort c nil_cert
175
[A,B,Bs,c,cs,ca]
Raphael Cauderlier's avatar
Raphael Cauderlier committed
176
    snoc_cert (fol.cons_sort _ _) A (cons_cert B Bs c cs) ca
177
      -->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
178
    cons_cert B (fol.snoc_sort Bs A) c (snoc_cert Bs A cs ca).
179 180


Raphael Cauderlier's avatar
Raphael Cauderlier committed
181 182
def f_equal_fun_n : L' : fol.sorts ->
                    L : fol.sorts ->
183 184 185
                    certificates L ->
                    f_equal_T L'.
[L,B,f,as,bs,cs]
Raphael Cauderlier's avatar
Raphael Cauderlier committed
186
    f_equal_fun_n fol.nil_sort L cs
187 188 189
      -->
    f_equal_fun_on_goal L cs
[A,As,L,B,f,as,bs,cs]
Raphael Cauderlier's avatar
Raphael Cauderlier committed
190
    f_equal_fun_n (fol.cons_sort A As) L cs
191 192
      -->
    c : certificate =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
193
    f_equal_fun_n As (fol.snoc_sort L A) (snoc_cert L A cs c).
194 195 196

def f_equal (f : fol.function) :=
  f_equal_fun_n
Raphael Cauderlier's avatar
Raphael Cauderlier committed
197
    (fol.fun_domain f)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
198
    fol.nil_sort
199 200
    nil_cert.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
201
(; 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
202
def rewrite (A : sort) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate
Raphael Cauderlier's avatar
Raphael Cauderlier committed
203 204
:=
  cert.with_goal (G =>
205
             cert.refine2 (eq A a b)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
206 207
                     (unif.subst_prop (unif.cons_subst A b a unif.empty_subst) G)
                     G
208
                       (Hab : proof (eq A a b) =>
209
                        eq.eq_congr A a b Hab (a =>
Raphael Cauderlier's avatar
Raphael Cauderlier committed
210 211 212 213
                             unif.subst_prop
                               (unif.cons_subst A b a unif.empty_subst) G))
                       c1
                       c2).