X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FCoq.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FCoq.ma;h=8b1c5bd3a84e37ff5043774d3eea109fd2fec9ec;hb=29714797b01e0ac8c22e4df2827b1785a759f482;hp=0000000000000000000000000000000000000000;hpb=1fb0f39de8b87920d2f15f9e33929d372fa518dd;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.ma b/helm/software/matita/contribs/procedural/Coq/Coq.ma
new file mode 100644
index 000000000..8b1c5bd3a
--- /dev/null
+++ b/helm/software/matita/contribs/procedural/Coq/Coq.ma
@@ -0,0 +1,813 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "preamble.ma".
+
+(* From Arith/Compare *****************************************************)
+
+(* NOTATION
+Notation not_eq_sym := sym_not_eq.
+*)
+
+(* From Bool/Bool *********************************************************)
+
+(* NOTATION
+Infix "||" := orb (at level 50, left associativity) : bool_scope.
+*)
+
+(* NOTATION
+Infix "&&" := andb (at level 40, left associativity) : bool_scope.
+*)
+
+(* From Init/Datatypes ****************************************************)
+
+(* NOTATION
+Add Printing If bool.
+*)
+
+(* NOTATION
+Notation "x + y" := (sum x y) : type_scope.
+*)
+
+(* NOTATION
+Add Printing Let prod.
+*)
+
+(* NOTATION
+Notation "x * y" := (prod x y) : type_scope.
+*)
+
+(* NOTATION
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+*)
+
+(* From Init/Logic ********************************************************)
+
+(* NOTATION
+Notation "~ x" := (not x) : type_scope.
+*)
+
+(* NOTATION
+Notation "A <-> B" := (iff A B) : type_scope.
+*)
+
+(* NOTATION
+Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
+  (at level 200) : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists' x , p" := (ex (fun x => p))
+  (at level 200, x ident) : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists' x : t , p" := (ex (fun x:t => p))
+  (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
+  : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
+  (at level 200, x ident, p at level 200) : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
+  (at level 200, x ident, t at level 200, p at level 200,
+   format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
+  : type_scope.
+*)
+
+(* NOTATION
+Notation "x = y" := (x = y :>_) : type_scope.
+*)
+
+(* NOTATION
+Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
+*)
+
+(* NOTATION
+Notation "x <> y" := (x <> y :>_) : type_scope.
+*)
+
+(* From Init/Notations ****************************************************)
+
+(* NOTATION
+Reserved Notation "x <-> y" (at level 95, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x /\ y" (at level 80, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x \/ y" (at level 85, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "~ x" (at level 75, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x = y  :> T"
+(at level 70, y at next level, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x = y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x = y = z"
+(at level 70, no associativity, y at next level).
+*)
+
+(* NOTATION
+Reserved Notation "x <> y  :> T"
+(at level 70, y at next level, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x <> y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x <= y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x < y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x >= y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x > y" (at level 70, no associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x <= y <= z" (at level 70, y at next level).
+*)
+
+(* NOTATION
+Reserved Notation "x <= y < z" (at level 70, y at next level).
+*)
+
+(* NOTATION
+Reserved Notation "x < y < z" (at level 70, y at next level).
+*)
+
+(* NOTATION
+Reserved Notation "x < y <= z" (at level 70, y at next level).
+*)
+
+(* NOTATION
+Reserved Notation "x + y" (at level 50, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x - y" (at level 50, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x * y" (at level 40, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x / y" (at level 40, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "- x" (at level 35, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "/ x" (at level 35, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "x ^ y" (at level 30, right associativity).
+*)
+
+(* NOTATION
+Reserved Notation "( x , y , .. , z )" (at level 0).
+*)
+
+(* NOTATION
+Reserved Notation "{ x }" (at level 0, x at level 99).
+*)
+
+(* NOTATION
+Reserved Notation "{ A } + { B }" (at level 50, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "A + { B }" (at level 50, left associativity).
+*)
+
+(* NOTATION
+Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
+*)
+
+(* NOTATION
+Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
+*)
+
+(* NOTATION
+Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
+*)
+
+(* NOTATION
+Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
+*)
+
+(* From Init/Peano ********************************************************)
+
+(* NOTATION
+Infix "+" := plus : nat_scope.
+*)
+
+(* NOTATION
+Infix "*" := mult : nat_scope.
+*)
+
+(* NOTATION
+Infix "-" := minus : nat_scope.
+*)
+
+(* NOTATION
+Infix "<=" := le : nat_scope.
+*)
+
+(* NOTATION
+Infix "<" := lt : nat_scope.
+*)
+
+(* NOTATION
+Infix ">=" := ge : nat_scope.
+*)
+
+(* NOTATION
+Infix ">" := gt : nat_scope.
+*)
+
+(* NOTATION
+Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
+*)
+
+(* From Init/Specif *******************************************************)
+
+(* NOTATION
+Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
+*)
+
+(* NOTATION
+Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
+  type_scope.
+*)
+
+(* NOTATION
+Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
+*)
+
+(* NOTATION
+Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
+  type_scope.
+*)
+
+(* NOTATION
+Add Printing Let sig.
+*)
+
+(* NOTATION
+Add Printing Let sig2.
+*)
+
+(* NOTATION
+Add Printing Let sigS.
+*)
+
+(* NOTATION
+Add Printing Let sigS2.
+*)
+
+(* NOTATION
+Add Printing If sumbool.
+*)
+
+(* NOTATION
+Add Printing If sumor.
+*)
+
+(* From Lists/List ********************************************************)
+
+(* NOTATION
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+*)
+
+(* NOTATION
+Infix "++" := app (right associativity, at level 60) : list_scope.
+*)
+
+(* NOTATION
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+*)
+
+(* NOTATION
+Infix "++" := app (right associativity, at level 60) : list_scope.
+*)
+
+(* From Num/Leibniz/EqAxioms **********************************************)
+
+(* NOTATION
+Grammar constr constr1 :=
+eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+*)
+
+(* NOTATION
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
+*)
+
+(* From Num/Leibniz/NSyntax ***********************************************)
+
+(* NOTATION
+Infix 6 "<" lt.
+*)
+
+(* NOTATION
+Infix 6 "<=" le.
+*)
+
+(* NOTATION
+Infix 6 ">" gt.
+*)
+
+(* NOTATION
+Infix 6 ">=" ge.
+*)
+
+(* NOTATION
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+*)
+
+(* NOTATION
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+ ;
+
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
+*)
+
+(* From Num/Nat/NSyntax ***************************************************)
+
+(* NOTATION
+Infix 6 "<" lt.
+*)
+
+(* NOTATION
+Infix 6 "<=" le.
+*)
+
+(* NOTATION
+Infix 6 ">" gt.
+*)
+
+(* NOTATION
+Infix 6 ">=" ge.
+*)
+
+(* NOTATION
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+*)
+
+(* NOTATION
+Syntax constr
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
+*)
+
+(* From Num/EqParams ******************************************************)
+
+(* NOTATION
+Grammar constr constr1 :=
+eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+*)
+
+(* NOTATION
+Syntax constr
+  level 1:
+    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+.
+*)
+
+(* From Num/NSyntax *******************************************************)
+
+(* NOTATION
+Infix 6 "<" lt V8only 70.
+*)
+
+(* NOTATION
+Infix 6 "<=" le V8only 70.
+*)
+
+(* NOTATION
+Infix 6 ">" gt V8only 70.
+*)
+
+(* NOTATION
+Infix 6 ">=" ge V8only 70.
+*)
+
+(* NOTATION
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+*)
+
+(* NOTATION
+Syntax constr
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
+*)
+
+(* From Num/NeqDef ********************************************************)
+
+(* NOTATION
+Infix 6 "<>" neq V8only 70.
+*)
+
+(* From Num/NeqParams *****************************************************)
+
+(* NOTATION
+Infix 6 "<>" neq V8only 70.
+*)
+
+(* From Reals/RIneq *******************************************************)
+
+(* NOTATION
+Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
+ with minus := Rminus div := Rdiv.
+*)
+
+(* From Reals/Ranalysis1 **************************************************)
+
+(* NOTATION
+Infix "+" := plus_fct : Rfun_scope.
+*)
+
+(* NOTATION
+Notation "- x" := (opp_fct x) : Rfun_scope.
+*)
+
+(* NOTATION
+Infix "*" := mult_fct : Rfun_scope.
+*)
+
+(* NOTATION
+Infix "-" := minus_fct : Rfun_scope.
+*)
+
+(* NOTATION
+Infix "/" := div_fct : Rfun_scope.
+*)
+
+(* NOTATION
+Notation Local "f1 'o' f2" := (comp f1 f2)
+  (at level 20, right associativity) : Rfun_scope.
+*)
+
+(* NOTATION
+Notation "/ x" := (inv_fct x) : Rfun_scope.
+*)
+
+(* From Reals/Rdefinitions ************************************************)
+
+(* NOTATION
+Infix "+" := Rplus : R_scope.
+*)
+
+(* NOTATION
+Infix "*" := Rmult : R_scope.
+*)
+
+(* NOTATION
+Notation "- x" := (Ropp x) : R_scope.
+*)
+
+(* NOTATION
+Notation "/ x" := (Rinv x) : R_scope.
+*)
+
+(* NOTATION
+Infix "<" := Rlt : R_scope.
+*)
+
+(* NOTATION
+Infix "-" := Rminus : R_scope.
+*)
+
+(* NOTATION
+Infix "/" := Rdiv : R_scope.
+*)
+
+(* NOTATION
+Infix "<=" := Rle : R_scope.
+*)
+
+(* NOTATION
+Infix ">=" := Rge : R_scope.
+*)
+
+(* NOTATION
+Infix ">" := Rgt : R_scope.
+*)
+
+(* NOTATION
+Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
+*)
+
+(* NOTATION
+Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
+*)
+
+(* NOTATION
+Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
+*)
+
+(* NOTATION
+Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
+*)
+
+(* From Reals/Rfunctions **************************************************)
+
+(* NOTATION
+Infix "^" := pow : R_scope.
+*)
+
+(* NOTATION
+Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
+*)
+
+(* From Reals/Rpower ******************************************************)
+
+(* NOTATION
+Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
+*)
+
+(* From Reals/Rtopology ***************************************************)
+
+(* NOTATION
+Infix "=_D" := eq_Dom (at level 70, no associativity).
+*)
+
+(* From Setoids/Setoid ****************************************************)
+
+(* NOTATION
+Add Setoid Prop iff Prop_S.
+*)
+
+(* From Wellfounded/Disjoint_Union ****************************************)
+
+(* NOTATION
+Notation Le_AsB := (le_AsB A B leA leB).
+*)
+
+(* From Wellfounded/Lexicographic_Product *********************************)
+
+(* NOTATION
+Notation LexProd := (lexprod A B leA leB).
+*)
+
+(* NOTATION
+Notation Symprod := (symprod A B leA leB).
+*)
+
+(* NOTATION
+Notation SwapProd := (swapprod A R).
+*)
+
+(* From Wellfounded/Union *************************************************)
+
+(* NOTATION
+Notation Union := (union A R1 R2).
+*)
+
+(* From Wellfounded/Lexicographic_Exponentiation **************************)
+
+(* NOTATION
+Notation Power := (Pow A leA).
+*)
+
+(* NOTATION
+Notation Lex_Exp := (lex_exp A leA).
+*)
+
+(* NOTATION
+Notation ltl := (Ltl A leA).
+*)
+
+(* NOTATION
+Notation Descl := (Desc A leA).
+*)
+
+(* NOTATION
+Notation List := (list A).
+*)
+
+(* NOTATION
+Notation Nil := (nil (A:=A)).
+*)
+
+(* NOTATION
+Notation Cons := (cons (A:=A)).
+*)
+
+(* NOTATION
+Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
+*)
+
+(* From Wellfounded/Transitive_Closure ************************************)
+
+(* NOTATION
+Notation trans_clos := (clos_trans A R).
+*)
+
+(* From ZArith/Zdiv *******************************************************)
+
+(* NOTATION
+Infix "/" := Zdiv : Z_scope.
+*)
+
+(* NOTATION
+Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
+*)
+
+(* From ZArith/Zpower *****************************************************)
+
+(* NOTATION
+Infix "^" := Zpower : Z_scope.
+*)
+
+(* NOTATION
+Infix "^" := Zpower : Z_scope.
+*)
+
+(* From ZArith/BinInt *****************************************************)
+
+(* NOTATION
+Infix "+" := Zplus : Z_scope.
+*)
+
+(* NOTATION
+Notation "- x" := (Zopp x) : Z_scope.
+*)
+
+(* NOTATION
+Infix "-" := Zminus : Z_scope.
+*)
+
+(* NOTATION
+Infix "*" := Zmult : Z_scope.
+*)
+
+(* NOTATION
+Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
+*)
+
+(* NOTATION
+Infix "<=" := Zle : Z_scope.
+*)
+
+(* NOTATION
+Infix "<" := Zlt : Z_scope.
+*)
+
+(* NOTATION
+Infix ">=" := Zge : Z_scope.
+*)
+
+(* NOTATION
+Infix ">" := Zgt : Z_scope.
+*)
+
+(* NOTATION
+Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
+*)
+
+(* NOTATION
+Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
+*)
+
+(* NOTATION
+Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
+*)
+
+(* NOTATION
+Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
+*)
+
+(* From ZArith/Znumtheory *************************************************)
+
+(* NOTATION
+Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
+*)
+
+(* From NArith/BinNat *****************************************************)
+
+(* NOTATION
+Infix "+" := Nplus : N_scope.
+*)
+
+(* NOTATION
+Infix "*" := Nmult : N_scope.
+*)
+
+(* NOTATION
+Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+*)
+
+(* From NArith/BinPos *****************************************************)
+
+(* NOTATION
+Infix "+" := Pplus : positive_scope.
+*)
+
+(* NOTATION
+Infix "-" := Pminus : positive_scope.
+*)
+
+(* NOTATION
+Infix "*" := Pmult : positive_scope.
+*)
+
+(* NOTATION
+Infix "/" := Pdiv2 : positive_scope.
+*)
+
+(* NOTATION
+Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
+*)
+