Bug fixed: the generated elimination principles used to have Anonymous

binders referenced! Fixed.

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d7b378c007017f008e49c71ee4eb56bc8c97f3cd..6ba305d98c05d2b8b50468f47dee83f5b8b41023 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -14,7 +14,8 @@
 
 set "baseuri" "cic:/matita/Z/".
 
-include "../nat/nat.ma".
+include "nat/nat.ma".
+include "datatypes/bool.ma".
 
 inductive Z : Set \def
   OZ : Z

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index af3ca38f83c0cd02478e8c85fc118e82d906a0ec..d148dfd310b2b8be46fdb8a5e4b854e71d6ac34f 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/compare.ma".
+set "baseuri" "cic:/matita/nat/compare".
 
 include "nat/orders.ma".
 include "datatypes/bool.ma".

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 4fa85a6bb4f6c901a28fcafcff0ad68d5def0a48..0091cb9b09b93ace2834862b1b84d64d7bdd219d 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/minus.ma".
+set "baseuri" "cic:/matita/nat/minus".
 
 include "nat/orders_op.ma".
 include "nat/times.ma".

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 4c1b1a0c4851b65b64140193a626c90c922bb7c0..1939b3c13764e4c9937dbe5af73a3bd09abb0dc2 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders.ma".
+set "baseuri" "cic:/matita/nat/orders".
 
 include "logic/connectives.ma".
 include "logic/equality.ma".
@@ -67,7 +67,7 @@ qed.
 
 theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
 intros.change with le (pred (S n)) (pred (S m)).
-elim H.apply le_n.apply trans_le ? (pred x).assumption.
+elim H.apply le_n.apply trans_le ? (pred e2).assumption.
 apply le_pred_n.
 qed.
 

diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index dbd48fa8852f6d91e2c31d33a675eeb4cb729e1d..801e123d2c901a65c7894c04fe71c9e5920700f6 100644 (file)
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders_op.ma".
+set "baseuri" "cic:/matita/nat/orders_op".
 
 include "higher_order_defs/functions.ma".
 include "nat/times.ma".

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 1a43e216f7f1a86f2c80713f39db3f13f7ab637f..fbb3fcc90b76e4ceb7b037336f3393336ccffea3 100644 (file)
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/plus.ma".
+set "baseuri" "cic:/matita/nat/plus".
 
 include "logic/equality.ma".
 include "nat/nat.ma".
@@ -73,4 +73,4 @@ assumption.
 qed.
 
 theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
-\def injective_plus_l.
\ No newline at end of file
+\def injective_plus_l.

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index f9c731bb0e4c85447cffb3d460358ddb9809d2c8..44f73b71a080b6e253d49b5dfbb2e1b622d45174 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times.ma".
+set "baseuri" "cic:/matita/nat/times".
 
 include "logic/equality.ma".
 include "nat/nat.ma".

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index 7163c56b390f28b0332910110c6494fe8716d93f..565a5c49aa88077cfabdc1b0c996959fdbe56f6f 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -53,7 +53,7 @@ qed.
 
 theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to 
                         (x = O).
-intros 3. elim H. auto. apply eq_gen_S_O. exact x2. auto.
+intros 3. elim H. auto. apply eq_gen_S_O. exact e3. auto.
 qed.
 
 theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
@@ -68,7 +68,7 @@ theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
                         (\exists n. x = (S n) \land (le m n)).
 intros 4. elim H. 
 apply eq_gen_S_O. exact m. elim H1. auto. 
-cut x1 = m. elim Hcut. apply ex_intro. exact x2. auto. auto.
+cut e4 = m. elim Hcut. apply ex_intro. exact e3. auto. auto.
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index c0552e79ee7385c38bbf3f0781c8895eab8897e3..eecb0fae6a97826e037e8c150b14d3493a0d7c67 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -32,12 +32,9 @@ let debug_print = fun _ -> ()
 
 let counter = ref ~-1 ;;
 
-let fresh_binder =
-  function
-    | true ->
-        incr counter;
-        Cic.Name ("e" ^ string_of_int !counter)
-    | _ -> Cic.Anonymous
+let fresh_binder () =
+ incr counter;
+ Cic.Name ("e" ^ string_of_int !counter)
 
   (** verifies if a given inductive type occurs in a term in target position *)
 let rec recursive uri typeno = function
@@ -104,13 +101,13 @@ let rec delta (uri, typeno) dependent paramsno consno t p args =
             (CicSubstitution.lift 1 p) [Cic.Rel 1]
         in
         let tgt = CicSubstitution.lift 1 tgt in
-        Cic.Prod (fresh_binder dependent, src,
+        Cic.Prod (fresh_binder (), src,
           Cic.Prod (Cic.Anonymous, phi,
             delta (uri, typeno) dependent paramsno consno tgt
               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
-        Cic.Prod (fresh_binder dependent, src,
+        Cic.Prod (fresh_binder (), src,
           delta (uri, typeno) dependent paramsno consno tgt
             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
   | _ -> assert false
@@ -137,6 +134,11 @@ let rec add_params binder indno ty eliminator =
   else
     match ty with
     | Cic.Prod (name, src, tgt) ->
+       let name =
+        match name with
+           Cic.Name _ -> name
+         | Cic.Anonymous -> fresh_binder ()
+       in
         binder name src (add_params binder (indno - 1) tgt eliminator)
     | _ -> assert false
 
@@ -154,7 +156,15 @@ let rec count_pi = function
 
 let rec type_of_p sort dependent leftno indty = function
   | Cic.Prod (n, src, tgt) when leftno = 0 ->
-      Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
+      let n =
+       if dependent then 
+        match n with
+           Cic.Name _ -> n
+         | Cic.Anonymous -> fresh_binder ()
+       else
+        n
+      in
+       Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
   | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
   | t ->
       if dependent then
@@ -164,14 +174,14 @@ let rec type_of_p sort dependent leftno indty = function
 
 let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
-      Cic.Prod (fresh_binder true,
+      Cic.Prod (fresh_binder (),
         CicSubstitution.lift_from liftfrom liftno src,
         add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
   | Cic.Prod (_, _, tgt) ->
       add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
   | t ->
       if dependent then
-        Cic.Prod (fresh_binder dependent,
+        Cic.Prod (fresh_binder (),
           CicSubstitution.lift_from (rightno + 1) liftno indty,
           Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
       else
@@ -185,15 +195,15 @@ let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
 let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
 function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
-      Cic.Lambda (fresh_binder true,
+      Cic.Lambda (fresh_binder (),
         CicSubstitution.lift_from liftfrom liftno src,
         add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
           case tgt)
   | Cic.Prod (_, _, tgt) ->
-      add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty
+      add_right_lambda true (strip - 1) liftno liftfrom rightno indty
         case tgt
   | t ->
-      Cic.Lambda (fresh_binder true,
+      Cic.Lambda (fresh_binder (),
         CicSubstitution.lift_from (rightno + 1) liftno indty, case)
 
 let rec branch (uri, typeno) insource paramsno t fix head args =
@@ -227,13 +237,13 @@ let rec branch (uri, typeno) insource paramsno t fix head args =
           let src = CicSubstitution.lift 1 src in
           branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
         in
-        Cic.Lambda (fresh_binder true, src,
+        Cic.Lambda (fresh_binder (), src,
           branch (uri, typeno) insource paramsno tgt
             (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1; phi]))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
-        Cic.Lambda (fresh_binder true, src,
+        Cic.Lambda (fresh_binder (), src,
           branch (uri, typeno) insource paramsno tgt
           (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1]))
@@ -332,7 +342,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
               (fun (_, constructor) acc ->
                 decr consno;
                 let p = Cic.Rel !consno in
-                Cic.Lambda (fresh_binder true,
+                Cic.Lambda (fresh_binder (),
                   (delta (uri, typeno) dependent leftno !consno
                     constructor p [mk_constructor !consno]),
                   acc))