Added examples.

diff --git a/helm/gTopLevel/esempi/and_implies_or.cic b/helm/gTopLevel/esempi/and_implies_or.cic
new file mode 100644 (file)
index 0000000..c47bf76
--- /dev/null
+++ b/helm/gTopLevel/esempi/and_implies_or.cic
@@ -0,0 +1,11 @@
+alias and  /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias conj /Coq/Init/Logic/Conjunction/and.ind#1/1/1
+
+alias or        /Coq/Init/Logic/Disjunction/or.ind#1/1
+alias or_introl /Coq/Init/Logic/Disjunction/or.ind#1/1/1
+alias or_intror /Coq/Init/Logic/Disjunction/or.ind#1/1/2
+
+\A:Prop.
+\B:Prop.
+\H:(and A B).
+ Case (H : and ; (or A B)) { \a:A.\b:B.(or_introl A B a) }

diff --git a/helm/gTopLevel/esempi/and_implies_or2.cic b/helm/gTopLevel/esempi/and_implies_or2.cic
new file mode 100644 (file)
index 0000000..f693df3
--- /dev/null
+++ b/helm/gTopLevel/esempi/and_implies_or2.cic
@@ -0,0 +1,8 @@
+alias and  /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias conj /Coq/Init/Logic/Conjunction/and.ind#1/1/1
+
+alias or        /Coq/Init/Logic/Disjunction/or.ind#1/1
+alias or_introl /Coq/Init/Logic/Disjunction/or.ind#1/1/1
+alias or_intror /Coq/Init/Logic/Disjunction/or.ind#1/1/2
+
+!A:Prop.!B:Prop.!H:(and A B).(or A B)

diff --git a/helm/gTopLevel/esempi/apply.cic b/helm/gTopLevel/esempi/apply.cic
new file mode 100644 (file)
index 0000000..fb27e16
--- /dev/null
+++ b/helm/gTopLevel/esempi/apply.cic
@@ -0,0 +1,21 @@
+alias nat    /Coq/Init/Datatypes/nat.ind#1/1
+alias eq     /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
+alias O      /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S      /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus   /Coq/Init/Peano/plus.con
+alias mult   /Coq/Init/Peano/mult.con
+alias le     /Coq/Init/Peano/le.ind#1/1
+alias lt     /Coq/Init/Peano/lt.con
+alias not    /Coq/Init/Logic/not.con
+(eq nat (\x:nat.\y:nat.O O O) (\x:nat.\y:nat.O O O))
+/Coq/Init/Logic/f_equal2.con
+/Coq/Init/Logic/Equality/eq.ind#1/1/1
+
+(*
+(le O (S O))
+/Coq/Arith/Gt/gt_S_le.con
+
+(not (lt O (plus O O)))
+/Coq/Arith/Lt/lt_n_n.con
+*)

diff --git a/helm/gTopLevel/esempi/bug.cic b/helm/gTopLevel/esempi/bug.cic
new file mode 100644 (file)
index 0000000..2f10c57
--- /dev/null
+++ b/helm/gTopLevel/esempi/bug.cic
@@ -0,0 +1,22 @@
+alias nat          /Coq/Init/Datatypes/nat.ind#1/1
+alias eqT          /Coq/Init/Logic_Type/eqT.ind#1/1
+alias eq           /Coq/Init/Logic/Equality/eq.ind#1/1
+alias refl_equal   /Coq/Init/Logic/Equality/eq.ind#1/1/1
+alias eq_ind       /Coq/Init/Logic/Equality/eq_ind.con
+alias eq_ind_r     /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias O            /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S            /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus         /Coq/Init/Peano/plus.con
+alias mult         /Coq/Init/Peano/mult.con
+alias le           /Coq/Init/Peano/le.ind#1/1
+alias lt           /Coq/Init/Peano/lt.con
+alias not          /Coq/Init/Logic/not.con
+alias f_equal      /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias le_trans     /Coq/Arith/Le/le_trans.con
+
+alias plus_n_O     /Coq/Init/Peano/plus_n_O.con 
+
+alias or           /Coq/Init/Logic/Disjunction/or.ind#1/1
+alias or_ind       /Coq/Init/Logic/Disjunction/or_ind.con
+
+(or (eq nat O O) (eq nat O O)) -> (lt O O)

diff --git a/helm/gTopLevel/esempi/calcolo_proposizioni.cic b/helm/gTopLevel/esempi/calcolo_proposizioni.cic
new file mode 100644 (file)
index 0000000..5fe90ed
--- /dev/null
+++ b/helm/gTopLevel/esempi/calcolo_proposizioni.cic
@@ -0,0 +1,17 @@
+alias True     /Coq/Init/Logic/True.ind#1/1
+alias I        /Coq/Init/Logic/True.ind#1/1/1
+alias True_ind /Coq/Init/Logic/True_ind.con
+
+alias False     /Coq/Init/Logic/False.ind#1/1
+alias False_ind /Coq/Init/Logic/False_ind.con
+
+alias and     /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias conj    /Coq/Init/Logic/Conjunction/and.ind#1/1/1
+alias and_ind /Coq/Init/Logic/Conjunction/and_ind.con
+
+alias or        /Coq/Init/Logic/Disjunction/or.ind#1/1
+alias or_introl /Coq/Init/Logic/Disjunction/or.ind#1/1/1
+alias or_intror /Coq/Init/Logic/Disjunction/or.ind#1/1/2
+alias or_ind    /Coq/Init/Logic/Disjunction/or_ind.con
+
+alias not          /Coq/Init/Logic/not.con

diff --git a/helm/gTopLevel/esempi/conversion.cic b/helm/gTopLevel/esempi/conversion.cic
new file mode 100644 (file)
index 0000000..3964f6f
--- /dev/null
+++ b/helm/gTopLevel/esempi/conversion.cic
@@ -0,0 +1,17 @@
+alias nat        /Coq/Init/Datatypes/nat.ind#1/1
+alias eqT        /Coq/Init/Logic_Type/eqT.ind#1/1
+alias eq         /Coq/Init/Logic/Equality/eq.ind#1/1
+alias refl_equal /Coq/Init/Logic/Equality/eq.ind#1/1/1
+alias eq_ind     /Coq/Init/Logic/Equality/eq_ind.con
+alias eq_ind_r   /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias O          /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S          /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus       /Coq/Init/Peano/plus.con
+alias mult       /Coq/Init/Peano/mult.con
+alias le         /Coq/Init/Peano/le.ind#1/1
+alias lt         /Coq/Init/Peano/lt.con
+alias not        /Coq/Init/Logic/not.con
+alias f_equal    /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+
+!n:nat.(eq nat (mult (S (S O)) n) O)
+!n:nat.(eq nat (plus O n) (plus n O))

diff --git a/helm/gTopLevel/esempi/elim.cic b/helm/gTopLevel/esempi/elim.cic
new file mode 100644 (file)
index 0000000..eb679d6
--- /dev/null
+++ b/helm/gTopLevel/esempi/elim.cic
@@ -0,0 +1,13 @@
+alias nat     /Coq/Init/Datatypes/nat.ind#1/1
+alias eq      /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eq_ind  /Coq/Init/Logic/Equality/eq_ind.con
+alias O       /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S       /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus    /Coq/Init/Peano/plus.con
+alias mult    /Coq/Init/Peano/mult.con
+alias le      /Coq/Init/Peano/le.ind#1/1
+alias lt      /Coq/Init/Peano/lt.con
+alias not     /Coq/Init/Logic/not.con
+alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+
+!n:nat.(eq nat (plus O n) (plus n O))

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
new file mode 100644 (file)
index 0000000..da77539
--- /dev/null
+++ b/helm/gTopLevel/esempi/elim2.cic
@@ -0,0 +1,36 @@
+alias nat        /Coq/Init/Datatypes/nat.ind#1/1
+alias eq         /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eq_ind     /Coq/Init/Logic/Equality/eq_ind.con
+alias eqT        /Coq/Init/Logic_Type/eqT.ind#1/1
+alias O          /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S          /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus       /Coq/Init/Peano/plus.con
+alias mult       /Coq/Init/Peano/mult.con
+alias le         /Coq/Init/Peano/le.ind#1/1
+alias lt         /Coq/Init/Peano/lt.con
+alias not        /Coq/Init/Logic/not.con
+alias and        /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias prod       /Coq/Init/Datatypes/prod.ind#1/1 
+alias list       /Coq/Lists/PolyList/Lists/list.ind#1/1
+alias AllS_assoc /Coq/Lists/TheoryList/Lists/Assoc_sec/AllS_assoc.ind#1/1
+
+!A:Set.!B:Set.!P:!a:A.Prop.!l:(list (prod A B)).
+ !H:(AllS_assoc A B P l).
+  (and
+   (eq (list (prod A B)) l l)
+   (eqT !n:A.Prop P P))
+
+(* Intros; Elim H:
+
+?1: (A,B:Set; P:(A->Prop); l:(list A*B))
+     (AllS_assoc A B P l) -> (nil A*B)=(nil A*B)/\P==P
+?2: (A,B:Set; P:(A->Prop); l:(list A*B))
+     (AllS_assoc A B P l) ->
+      (a:A; b:B; l0:(list A*B))
+       (P a) -> (AllS_assoc A B P l0) -> l0=l0/\P==P ->
+        (cons (a,b) l0)=(cons (a,b) l0)/\P==P
+[A,B:Set; P:(A->Prop); l:(list A*B); H:(AllS_assoc A B P l)]
+ (AllS_assoc_ind A B P [l0:(list A*B)]l0=l0/\P==P
+  (?1 A B P l H) (?2 A B P l H) l H)
+
+*)

diff --git a/helm/gTopLevel/esempi/evars.cic b/helm/gTopLevel/esempi/evars.cic
new file mode 100644 (file)
index 0000000..9183cb1
--- /dev/null
+++ b/helm/gTopLevel/esempi/evars.cic
@@ -0,0 +1,33 @@
+alias nat          /Coq/Init/Datatypes/nat.ind#1/1
+alias eqT          /Coq/Init/Logic_Type/eqT.ind#1/1
+alias eq           /Coq/Init/Logic/Equality/eq.ind#1/1
+alias refl_equal   /Coq/Init/Logic/Equality/eq.ind#1/1/1
+alias eq_ind       /Coq/Init/Logic/Equality/eq_ind.con
+alias eq_ind_r     /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias O            /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S            /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus         /Coq/Init/Peano/plus.con
+alias mult         /Coq/Init/Peano/mult.con
+alias le           /Coq/Init/Peano/le.ind#1/1
+alias lt           /Coq/Init/Peano/lt.con
+alias not          /Coq/Init/Logic/not.con
+alias f_equal      /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias le_trans     /Coq/Arith/Le/le_trans.con
+
+alias le_plus_plus /Coq/Arith/Plus/le_plus_plus.con
+alias le_reg_r     /Coq/Arith/Plus/le_reg_r.con
+alias le_reg_l     /Coq/Arith/Plus/le_reg_l.con
+
+alias plus_n_O     /Coq/Init/Peano/plus_n_O.con 
+
+!n:nat.!m:nat.(le n m)->(le (mult (S (S O)) n) (mult (S (S O)) m))
+
+(* Lo scopo dell'esercizio e' riuscire a effettuare la dimostrazione che *)
+(* (n <= m) -> (2*n <= 2*m) come la si farebbe su carta, ovvero:         *)
+(*                                                                       *)
+(*     2 * n                                                             *)
+(*  == n + n + 0     Simpl                                               *)
+(*  <= m + n + 0     le_reg_r because n <= m because hypothesis          *)
+(*  <= m + m + 0     le_reg_l because n + 0 <= m + 0 because le_reg_r    *)
+(*                    because hypothesis                                 *)
+(*  == 2 * m         Change                                              *)

diff --git a/helm/gTopLevel/esempi/prova.cic b/helm/gTopLevel/esempi/prova.cic
new file mode 100644 (file)
index 0000000..6ca06a8
--- /dev/null
+++ b/helm/gTopLevel/esempi/prova.cic
@@ -0,0 +1,16 @@
+alias eq   /Coq/Init/Logic/Equality/eq.ind#1/1
+alias nat  /Coq/Init/Datatypes/nat.ind#1/1
+alias O    /Coq/Init/Datatypes/nat.ind#1/1/1
+alias S    /Coq/Init/Datatypes/nat.ind#1/1/2
+alias plus /Coq/Init/Peano/plus.con
+alias mult /Coq/Init/Peano/mult.con
+(mult (plus (S (S O)) (S O)) (S (S O)))
+Case ((S O) : nat ; nat) { O ; \x:nat.x }
+Fix f {f(0) : !x:nat.nat ; g(0) : !x:nat.nat}
+ { \x:nat.O
+ ; \x:nat.
+    Case (x : nat ; nat) { (S O) ; \x:nat.(f x) }
+ }
+
+(* Nel caso seguente sbagliavamo a fare la whd!!!! *)
+!n:nat.(eq nat O (Case (n : nat ; \z:nat.!a:nat.nat) {\x:nat.x ; \y:nat.\x:nat.x} O))

diff --git a/helm/gTopLevel/esempi/ring/0eq0.cic b/helm/gTopLevel/esempi/ring/0eq0.cic
new file mode 100644 (file)
index 0000000..0b6f8f2
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/0eq0.cic
@@ -0,0 +1,10 @@
+(* prova di 0 == 0 *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+(eqT R R0 R0)

diff --git a/helm/gTopLevel/esempi/ring/aliases.cic b/helm/gTopLevel/esempi/ring/aliases.cic
new file mode 100644 (file)
index 0000000..f3fb95c
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/aliases.cic
@@ -0,0 +1,24 @@
+alias false /Coq/Init/Datatypes/bool.ind#1/1/2
+alias apolynomial_normalize_ok /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con
+alias RTheory /Coq/Reals/Rbase/RTheory.con
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3

diff --git a/helm/gTopLevel/esempi/ring/caso0.cic b/helm/gTopLevel/esempi/ring/caso0.cic
new file mode 100644 (file)
index 0000000..afe37f5
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso0.cic
@@ -0,0 +1,23 @@
+(* OK, meglio di coq *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R R1 R1)

diff --git a/helm/gTopLevel/esempi/ring/caso1.cic b/helm/gTopLevel/esempi/ring/caso1.cic
new file mode 100644 (file)
index 0000000..250e8cb
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso1.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  R1
+  (Rmult R1 R1))

diff --git a/helm/gTopLevel/esempi/ring/caso2.cic b/helm/gTopLevel/esempi/ring/caso2.cic
new file mode 100644 (file)
index 0000000..c9c3896
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso2.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rmult R1 R1)
+  R1)

diff --git a/helm/gTopLevel/esempi/ring/caso3.1.cic b/helm/gTopLevel/esempi/ring/caso3.1.cic
new file mode 100644 (file)
index 0000000..0d698cd
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso3.1.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rmult R1 R1)
+  (Rplus R1 R1))

diff --git a/helm/gTopLevel/esempi/ring/caso3.1bis.cic b/helm/gTopLevel/esempi/ring/caso3.1bis.cic
new file mode 100644 (file)
index 0000000..ec85c07
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso3.1bis.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rplus R1 R1)
+  (Rmult R1 R1))

diff --git a/helm/gTopLevel/esempi/ring/caso3.2.cic b/helm/gTopLevel/esempi/ring/caso3.2.cic
new file mode 100644 (file)
index 0000000..d6d0b5a
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso3.2.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rmult (Rplus R1 R1) R1)
+  (Rmult R1 (Rplus R1 R1)))

diff --git a/helm/gTopLevel/esempi/ring/caso3.3.cic b/helm/gTopLevel/esempi/ring/caso3.3.cic
new file mode 100644 (file)
index 0000000..0ac953a
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/caso3.3.cic
@@ -0,0 +1,25 @@
+(* ok *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R
+  (Rmult (Rplus R1 R1) R1)
+  (Rmult R1 R1))

diff --git a/helm/gTopLevel/esempi/ring/coq_overkill_helm_rulez.cic b/helm/gTopLevel/esempi/ring/coq_overkill_helm_rulez.cic
new file mode 100644 (file)
index 0000000..f7879b5
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/coq_overkill_helm_rulez.cic
@@ -0,0 +1,23 @@
+(* meglio di coq *)
+alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R             /Coq/Reals/Rdefinitions/R.con
+alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
+alias R1            /Coq/Reals/Rdefinitions/R1.con
+alias R0            /Coq/Reals/Rdefinitions/R0.con
+alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
+alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
+alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
+alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
+alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
+alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
+alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
+alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
+alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
+alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
+alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
+alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
+alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
+alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
+(eqT R R1 R0)

diff --git a/helm/gTopLevel/esempi/ring/novarmap.cic b/helm/gTopLevel/esempi/ring/novarmap.cic
new file mode 100644 (file)
index 0000000..63deeff
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/novarmap.cic
@@ -0,0 +1,13 @@
+(* Goal ``-1 + 1*2 == 2*0 + 1`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+(eqT R
+  (Rplus (Ropp R1) (Rmult R1 (Rplus R1 R1)))
+  (Rplus (Rmult (Rplus R1 R1) R0) R1)
+)

diff --git a/helm/gTopLevel/esempi/ring/novarmap_tofinish.cic b/helm/gTopLevel/esempi/ring/novarmap_tofinish.cic
new file mode 100644 (file)
index 0000000..1a335f3
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/novarmap_tofinish.cic
@@ -0,0 +1,13 @@
+(* Goal: ``1 = 2`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+(eqT R
+  R1
+  (Rplus R1 R1)
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap.cic b/helm/gTopLevel/esempi/ring/varmap.cic
new file mode 100644 (file)
index 0000000..d2cf450
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap.cic
@@ -0,0 +1,14 @@
+(* Goal: ``x+y == 2*y+(x-y)`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!x:R.!y:R.
+(eqT R
+  (Rplus x y)
+  (Rplus (Rmult (Rplus R1 R1) y) (Rplus x (Ropp y)))
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap2.cic b/helm/gTopLevel/esempi/ring/varmap2.cic
new file mode 100644 (file)
index 0000000..d3aa6c8
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap2.cic
@@ -0,0 +1,14 @@
+(* Goal: ``x+y == x+y+x`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!x:R.!y:R.
+(eqT R
+  (Rplus x y)
+  (Rplus (Rplus x y) x)
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap_trivial.cic b/helm/gTopLevel/esempi/ring/varmap_trivial.cic
new file mode 100644 (file)
index 0000000..15e2a51
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap_trivial.cic
@@ -0,0 +1,14 @@
+(* Goal (x,y:R)``x+y==y+x`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!x:R.!y:R.
+(eqT R
+  (Rplus x y)
+  (Rplus y x)
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap_trivial2.cic b/helm/gTopLevel/esempi/ring/varmap_trivial2.cic
new file mode 100644 (file)
index 0000000..e05aecd
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap_trivial2.cic
@@ -0,0 +1,14 @@
+(* Goal (x,y,z:R)``x+y+z==z+y+x`` *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!x:R.!y:R.!z:R.
+(eqT R
+  (Rplus (Rplus x y) z)
+  (Rplus (Rplus z y) x)
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap_trivial3.cic b/helm/gTopLevel/esempi/ring/varmap_trivial3.cic
new file mode 100644 (file)
index 0000000..c1bb161
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap_trivial3.cic
@@ -0,0 +1,14 @@
+(* Goal (x:R)``2*x==x+x``. *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!x:R.
+(eqT R
+  (Rmult (Rplus R1 R1) x)
+  (Rplus x x)
+)

diff --git a/helm/gTopLevel/esempi/ring/varmap_trivial_molte_variabili.cic b/helm/gTopLevel/esempi/ring/varmap_trivial_molte_variabili.cic
new file mode 100644 (file)
index 0000000..ce9d86d
--- /dev/null
+++ b/helm/gTopLevel/esempi/ring/varmap_trivial_molte_variabili.cic
@@ -0,0 +1,14 @@
+(* Goal (u,v,w,x,y,z:R)``u+v+w+x+y+z==z+y+x+w+v+u``. *)
+alias eq        /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
+alias R         /Coq/Reals/Rdefinitions/R.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rmult     /Coq/Reals/Rdefinitions/Rmult.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
+alias Ropp      /Coq/Reals/Rdefinitions/Ropp.con
+!u:R.!v:R.!w:R.!x:R.!y:R.!z:R.
+(eqT R
+  (Rplus (Rplus (Rplus (Rplus (Rplus u v) w) x) y) z)
+  (Rplus (Rplus (Rplus (Rplus (Rplus z y) x) w) v) u)
+)

diff --git a/helm/gTopLevel/esempi/sets.cic b/helm/gTopLevel/esempi/sets.cic
new file mode 100644 (file)
index 0000000..156e231
--- /dev/null
+++ b/helm/gTopLevel/esempi/sets.cic
@@ -0,0 +1,15 @@
+Open:
+/Coq/Sets/Powerset_facts/Sets_as_an_algebra/Union_commutative.con
+
+We prove the conjunction again:
+
+alias Ensemble /Coq/Sets/Ensembles/Ensembles/Ensemble.con
+alias Union    /Coq/Sets/Ensembles/Ensembles/Union.ind#1/1
+alias Included /Coq/Sets/Ensembles/Ensembles/Included.con
+alias and      /Coq/Init/Logic/Conjunction/and.ind#1/1
+
+The two parts of the conjunction can be proved in the same way. So we
+can make a Cut:
+
+!V:Set.!C:(Ensemble V).!D:(Ensemble V).(Included V (Union V C D)
+(Union V D C))