From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 09:52:37 +0000 (+0000) Subject: Bug fixed: the generated elimination principles used to have Anonymous X-Git-Tag: pre_notation~54 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f263e4ec717d5ec2e7f9c057855f8223f81baae8;p=helm.git 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 d7b378c00..6ba305d98 100644 --- 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 af3ca38f8..d148dfd31 100644 --- 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 4fa85a6bb..0091cb9b0 100644 --- 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 4c1b1a0c4..1939b3c13 100644 --- 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 dbd48fa88..801e123d2 100644 --- 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 1a43e216f..fbb3fcc90 100644 --- 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 f9c731bb0..44f73b71a 100644 --- 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 7163c56b3..565a5c49a 100644 --- 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 c0552e79e..eecb0fae6 100644 --- 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))