matita/matita/contribs/lambdadelta/apps_2/etc/models/valign.etc

   1 include "apps_2/notation/models/upspoon_3.ma".
   2
   3    al: nat → dd → dd;                      (* alignment *)
   4
   5 interpretation "alignment (model)"
   6    'UpSpoon M i d = (al M i d).
   7
   8 (* Note: lift: compatibility *)
   9    mf: compatible_3 … (al M) (eq …) (sq M) (sq M);
  10 (* Note: lift: swap *)
  11    mw: ∀l1,l2,d. l2 ≤ l1 → ⫯[l2]⫯[l1]d ≗{M} ⫯[↑l1]⫯[l2]d;
  12 (* Note: lift: sort evaluation *)
  13    mv: ∀l,s. ⫯[l](sv M s) ≗ sv M s;
  14
  15 theorem valign_swap (M): is_model M →
  16                          ∀l1,l2. l2 ≤ l1 →
  17                          ∀lv:evaluation ….  ⫯[l2]⫯[l1]lv ≗{M} ⫯[↑l1]⫯[l2]lv.
  18 /2 width=1 by mw/ qed.
  19
  20 lemma valign_comp (M): is_model M →
  21                        ∀l. compatible_2 … (valign M l) (veq M) (veq M).
  22 /2 width=1 by mf/ qed-.