matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Legacy-1/definitions.ma".
  16
  17 default "equality"
  18  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
  19  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/sym_eq.con
  20  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/trans_eq.con
  21  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_ind.con
  22  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_ind_r.con
  23  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rec.con
  24  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rec_r.con
  25  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con
  26  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rect_r.con
  27  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con
  28  cic:/matita/LAMBDA-TYPES/Legacy-2/preamble/f_equal_sym.con.
  29
  30 default "true"
  31  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True.ind.
  32 default "false"
  33  cic:/matita/LAMBDA-TYPES/Legacy-1/preamble/False.ind.
  34 default "absurd"
  35  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/absurd.con.
  36
  37 interpretation "Coq 7.3.1 natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
  38 interpretation "Coq 7.3.1 natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
  39 interpretation "Coq 7.3.1 logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
  40 interpretation "Coq 7.3.1 logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
  41 interpretation "Coq 7.3.1 logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
  42 interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
  43 interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
  44 interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
  45 interpretation "Coq 7.3.1 leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
  46
  47 alias symbol "plus" = "Coq 7.3.1 natural plus".
  48 alias symbol "minus" = "Coq 7.3.1 natural minus".
  49 alias symbol "and" = "Coq 7.3.1 logical and".
  50 alias symbol "or" = "Coq 7.3.1 logical or".
  51 alias symbol "not" = "Coq 7.3.1 logical not".
  52 alias symbol "exists" = "Coq 7.3.1 exists".
  53 alias symbol "leq" = "Coq 7.3.1 natural 'less or equal to'".
  54 alias symbol "lt" = "Coq 7.3.1 natural 'less than'".
  55 alias symbol "eq" = "Coq 7.3.1 leibnitz's equality".
  56
  57 theorem f_equal_sym: \forall A,B:Set.\forall f:A\to B.\forall x,y.
  58                      x = y \to (f y) = (f x).
  59   intros; symmetry.
  60   apply cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con.
  61   assumption.
  62 qed.