From: Stefano Zacchiroli Date: Tue, 2 Jul 2002 09:26:09 +0000 (+0000) Subject: Added examples. X-Git-Tag: V_0_3_0_debian_8~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fde1a6daa3aaa72c5c7536f4d2c65a3873b1c1bc;p=helm.git Added examples. --- diff --git a/helm/gTopLevel/esempi/and_implies_or.cic b/helm/gTopLevel/esempi/and_implies_or.cic new file mode 100644 index 000000000..c47bf76b6 --- /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 index 000000000..f693df30c --- /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 index 000000000..fb27e1693 --- /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 index 000000000..2f10c572c --- /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 index 000000000..5fe90ed32 --- /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 index 000000000..3964f6f12 --- /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 index 000000000..eb679d686 --- /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 index 000000000..da7753966 --- /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 index 000000000..9183cb1e4 --- /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 index 000000000..6ca06a862 --- /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 index 000000000..0b6f8f22e --- /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 index 000000000..f3fb95c0b --- /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 index 000000000..afe37f563 --- /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 index 000000000..250e8cbeb --- /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 index 000000000..c9c389674 --- /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 index 000000000..0d698cd48 --- /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 index 000000000..ec85c071a --- /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 index 000000000..d6d0b5ad8 --- /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 index 000000000..0ac953aa3 --- /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 index 000000000..f7879b576 --- /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 index 000000000..63deeff13 --- /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 index 000000000..1a335f3b2 --- /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 index 000000000..d2cf450b3 --- /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 index 000000000..d3aa6c85b --- /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 index 000000000..15e2a512b --- /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 index 000000000..e05aecd89 --- /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 index 000000000..c1bb161b8 --- /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 index 000000000..ce9d86da0 --- /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 index 000000000..156e231a2 --- /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))