From bc2720d7f2889d3df4cbb3c96d9929974092bda1 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 7 Feb 2007 20:31:40 +0000 Subject: Fix mistake naming my Tactics file Tactics :) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9624 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend.coq | 1 + Makefile | 2 +- contrib/subtac/SubtacTactics.v | 22 +++++++++++++++++ contrib/subtac/Tactics.v | 22 ----------------- contrib/subtac/subtac_coercion.ml | 51 ++++++++++++++++----------------------- 5 files changed, 45 insertions(+), 53 deletions(-) create mode 100644 contrib/subtac/SubtacTactics.v delete mode 100644 contrib/subtac/Tactics.v diff --git a/.depend.coq b/.depend.coq index 2b627f7c25..c094104971 100644 --- a/.depend.coq +++ b/.depend.coq @@ -362,6 +362,7 @@ contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo +contrib/subtac/SubtacTactics.vo: contrib/subtac/SubtacTactics.v contrib/subtac/Utils.vo: contrib/subtac/Utils.v theories/Logic/ProofIrrelevance.vo contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo contrib/subtac/Utils.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo contrib/subtac/Subtac.vo: contrib/subtac/Subtac.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo diff --git a/Makefile b/Makefile index 4b8580d66f..605239130a 100644 --- a/Makefile +++ b/Makefile @@ -1101,7 +1101,7 @@ JPROVERVO= CCVO= -SUBTACVO=contrib/subtac/Tactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ +SUBTACVO=contrib/subtac/SubtacTactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ contrib/subtac/FunctionalExtensionality.vo RTAUTOVO = \ diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v new file mode 100644 index 0000000000..25d8d8319d --- /dev/null +++ b/contrib/subtac/SubtacTactics.v @@ -0,0 +1,22 @@ +Ltac induction_with_subterm c H := + let x := fresh "x" in + let y := fresh "y" in + (set(x := c) ; assert(y:x = c) by reflexivity ; + rewrite <- y in H ; + induction H ; subst). + +Ltac induction_on_subterm c := + let x := fresh "x" in + let y := fresh "y" in + (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; + clear y). + +Ltac induction_with_subterms c c' H := + let x := fresh "x" in + let y := fresh "y" in + let z := fresh "z" in + let w := fresh "w" in + (set(x := c) ; assert(y:x = c) by reflexivity ; + set(z := c') ; assert(w:z = c') by reflexivity ; + rewrite <- y in H ; rewrite <- w in H ; + induction H ; subst). diff --git a/contrib/subtac/Tactics.v b/contrib/subtac/Tactics.v deleted file mode 100644 index 25d8d8319d..0000000000 --- a/contrib/subtac/Tactics.v +++ /dev/null @@ -1,22 +0,0 @@ -Ltac induction_with_subterm c H := - let x := fresh "x" in - let y := fresh "y" in - (set(x := c) ; assert(y:x = c) by reflexivity ; - rewrite <- y in H ; - induction H ; subst). - -Ltac induction_on_subterm c := - let x := fresh "x" in - let y := fresh "y" in - (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; - clear y). - -Ltac induction_with_subterms c c' H := - let x := fresh "x" in - let y := fresh "y" in - let z := fresh "z" in - let w := fresh "w" in - (set(x := c) ; assert(y:x = c) by reflexivity ; - set(z := c') ; assert(w:z = c') by reflexivity ; - rewrite <- y in H ; rewrite <- w in H ; - induction H ; subst). diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 30fd8281e1..38a95e9bc0 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -122,6 +122,22 @@ module Coercion = struct with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let rec coerce_application typ c c' l l' = + let rec aux typ i co = + trace (str"Inserting coercion at application"); + if i < Array.length l then + let hdx = l.(i) and hdy = l'.(i) in + let (n, eqT, restT) = destProd typ in + let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential dummy_loc env isevars eq in + let eq_app x = mkApp (Lazy.force eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) + in + aux (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in aux typ 0 (fun x -> x) + in (* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y); *) (* with _ -> ()); *) @@ -214,39 +230,14 @@ module Coercion = struct mkApp (prod.intro, [| a'; b'; x ; y |])) end else - (* if len = 1 && len = Array.length l' && i = i' then *) -(* let argx, argy = l.(0), l'.(0) in *) -(* let indtyp = Inductiveops.type_of_inductive env i in *) -(* let argname, argtype, _ = destProd indtyp in *) -(* let eq = *) -(* mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *) -(* in *) -(* let pred = mkLambda (argname, argtype, *) -(* mkApp (mkInd i, [| mkRel 1 |])) *) -(* in *) -(* let evar = make_existential dummy_loc env isevars eq in *) -(* Some (fun x -> *) -(* mkApp (Lazy.force eqrec, *) -(* [| argtype; argx; pred; x; argy; evar |])) *) -(* else *)subco () + if i = i' && len = Array.length l' then + Some (coerce_application (Typing.type_of env (evars_of !isevars) c) c c' l l') + else + subco () | x, y when x = y -> let lam_type = Typing.type_of env (evars_of !isevars) c in - let rec coerce typ i co = - if i < Array.length l then - let hdx = l.(i) and hdy = l'.(i) in - let (n, eqT, restT) = destProd typ in - let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in - let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in - let evar = make_existential dummy_loc env isevars eq in - let eq_app x = mkApp (Lazy.force eq_rect, - [| eqT; hdx; pred; x; hdy; evar|]) - in - coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) - else co - in if Array.length l = Array.length l' then ( - trace (str"Inserting coercion at application"); - Some (coerce lam_type 0 (fun x -> x)) + Some (coerce_application lam_type c c' l l') ) else subco () | _ -> subco ()) | _, _ -> subco () -- cgit v1.2.3