helm/software/matita/tests/push_pop_status.ma

   1
   2 (* XXX coercions *)
   3 axiom A: Type.
   4 axiom B: Type.
   5 axiom cAB: A -> B.
   6 coercion cic:/matita/tests/push_pop_status/cAB.con.
   7
   8 inductive eq (A:Type) (x:A) : A \to Prop \def
   9     refl_eq : eq A x x.
  10
  11 (* XXX notation *)
  12 notation "hvbox(a break === b)" non associative with precedence 45 for @{ 'eqqq $a $b }.
  13 interpretation "test" 'eqqq x y = (cic:/matita/tests/push_pop_status/eq.ind#xpointer(1/1) _ x y).
  14
  15 theorem eq_rect':
  16  \forall A. \forall x:A. \forall P: \forall y:A. x===y \to Type.
  17   P ? (refl_eq ? x) \to \forall y:A. \forall p:x===y. P y p.
  18  intros.
  19  exact
  20   (match p1 return \lambda y. \lambda p.P y p with
  21     [refl_eq \Rightarrow p]).
  22 qed.
  23
  24 lemma sym_eq : \forall A:Type.\forall x,y:A. x===y  \to y===x.
  25 intros.elim H. apply refl_eq.
  26 qed.
  27
  28 lemma trans_eq : \forall A:Type.\forall x,y,z:A. x===y  \to y===z \to x===z.
  29 intros.elim H1.assumption.
  30 qed.
  31
  32 theorem eq_elim_r:
  33  \forall A:Type.\forall x:A. \forall P: A \to Prop.
  34    P x \to \forall y:A. y===x \to P y.
  35 intros. elim (sym_eq ? ? ? H1).assumption.
  36 qed.
  37
  38 theorem eq_elim_r':
  39  \forall A:Type.\forall x:A. \forall P: A \to Set.
  40    P x \to \forall y:A. y===x \to P y.
  41 intros. elim (sym_eq ? ? ? H).assumption.
  42 qed.
  43
  44 theorem eq_elim_r'':
  45  \forall A:Type.\forall x:A. \forall P: A \to Type.
  46    P x \to \forall y:A. y===x \to P y.
  47 intros. elim (sym_eq ? ? ? H).assumption.
  48 qed.
  49
  50 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
  51 \forall x,y:A. x===y \to f x === f y.
  52 intros.elim H.apply refl_eq.
  53 qed.
  54
  55 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
  56 \forall x,y:A. x===y \to f y === f x.
  57 intros.elim H.apply refl_eq.
  58 qed.
  59
  60 (* XXX defaults *)
  61 default "equality"
  62  cic:/matita/tests/push_pop_status/eq.ind
  63  cic:/matita/tests/push_pop_status/sym_eq.con
  64  cic:/matita/tests/push_pop_status/trans_eq.con
  65  cic:/matita/tests/push_pop_status/eq_ind.con
  66  cic:/matita/tests/push_pop_status/eq_elim_r.con
  67  cic:/matita/tests/push_pop_status/eq_rec.con
  68  cic:/matita/tests/push_pop_status/eq_elim_r'.con
  69  cic:/matita/tests/push_pop_status/eq_rect.con
  70  cic:/matita/tests/push_pop_status/eq_elim_r''.con
  71  cic:/matita/tests/push_pop_status/eq_f.con
  72  cic:/matita/tests/push_pop_status/eq_f'.con. (* \x.sym (eq_f x) *)
  73
  74 include "push_pop_status_aux1.ma".
  75 (* include "push_pop_status_aux2.ma". *)
  76
  77 (* XXX default *)
  78 theorem prova: \forall x:A. eq A x x.
  79 intros. reflexivity.
  80 qed.
  81
  82 (* XXX notation *)
  83 theorem prova1: \forall x:A. x === x.
  84 intros. apply refl_eq.
  85 qed.
  86
  87 (* XXX coercion *)
  88 theorem pippo: A -> B.
  89 intro a.
  90 apply (a : B).
  91 qed.
  92
  93 definition X := b.
  94
  95