Procedural : added some missing cases

LAMBDA-TYPES: improved preambles

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 483378ce6c47f6f6df337687d71e133624bf9bd3..c004fd346b4e2a9ff30714fa3cf84af50a5acf00 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -321,6 +321,11 @@ and proc_mutconstruct st what =
    let script = [T.Apply (what, dtext)] in 
    mk_intros st what script
 
+and proc_const st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st what script
+
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
@@ -388,6 +393,7 @@ and proc_proof st t =
       | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
       | C.ARel _ as what                    -> proc_rel (f st) what
       | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what
+      | C.AConst _ as what                  -> proc_const (f st) what
       | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
       | what                                -> proc_other (f st) what
 
@@ -418,7 +424,8 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =   
+let is_theorem pars =
+   pars = [] ||
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
index 5bf2f44ef61b2e67060439408e2c106195174026..114efbd53479edff13a2103421c2283d46a30219 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "Base-1/definitions.ma".
+include "Legacy-2/theory.ma".
 
 alias symbol "minus" = "Coq's natural minus".
 alias symbol "lt" = "Coq's natural 'less than'".

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index 269e41d6aef9e114e92fd806edcc2ccf105df68f..a2c8a84ed1358d82d02d60b2a1c5694c54af07d1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -13,28 +13,40 @@
 (**************************************************************************)
 
 include "Legacy-1/definitions.ma".
-(*
+
 default "equality"
- cic:/Coq/Init/Logic/eq.ind
- cic:/Coq/Init/Logic/sym_eq.con
- cic:/Coq/Init/Logic/trans_eq.con
- cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/Coq/Init/Logic/eq_rec.con
- cic:/Coq/Init/Logic/eq_rec_r.con
- cic:/Coq/Init/Logic/eq_rect.con
- cic:/Coq/Init/Logic/eq_rect_r.con
- cic:/Coq/Init/Logic/f_equal.con
- cic:/matita/legacy/coq/f_equal1.con.
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/sym_eq.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/trans_eq.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_ind.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_ind_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rec.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rec_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/eq_rect_r.con
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con
+ cic:/matita/LAMBDA-TYPES/Legacy-2/preamble/f_equal_sym.con.
 
 default "true"
- cic:/Coq/Init/Logic/True.ind. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True.ind. 
 default "false"
- cic:/Coq/Init/Logic/False.ind. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/preamble/False.ind. 
 default "absurd"
- cic:/Coq/Init/Logic/absurd.con. 
+ cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/absurd.con. 
 
-(* aritmetic operators *)
+interpretation "Coq's natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
+interpretation "Coq's natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
+interpretation "Coq's logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
+interpretation "Coq's logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
+interpretation "Coq's logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
+interpretation "Coq's exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
+interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
+interpretation "Coq's natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
+interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
 
-interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
-*)
+theorem f_equal_sym: \forall A,B:Set.\forall f:A\to B.\forall x,y.
+                     x = y \to (f y) = (f x).
+  intros; symmetry.
+  apply cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/f_equal.con.
+  assumption.
+qed.