aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_cases.ml2
-rw-r--r--contrib/subtac/subtac_coercion.ml33
-rw-r--r--lib/util.ml4
-rw-r--r--test-suite/success/dependentind.v8
-rw-r--r--test-suite/success/setoid_test2.v4
-rw-r--r--theories/Program/Equality.v16
-rw-r--r--theories/Program/Subset.v10
-rw-r--r--theories/Program/Wf.v3
8 files changed, 44 insertions, 36 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6a470afc6..45f0f0129 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1977,7 +1977,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
(lift (nargeqs + nar) arg),
mk_eq_refl argt arg)
else
- (mk_JMeq (lift (nargeqs + slift) appt)
+ (mk_JMeq (lift (nargeqs + slift) t)
(mkRel (nargeqs + slift))
(lift (nargeqs + nar) argt)
(lift (nargeqs + nar) arg),
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 5ca313d0b..4a1869053 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -129,9 +129,9 @@ module Coercion = struct
with Reduction.NotConvertible -> coerce' env x 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 coerce_application typ typ' c c' l l' =
let len = Array.length l in
- let rec aux tele typ i co =
+ let rec aux tele typ typ' i co =
(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
(* str " to "++ my_print_constr env y *)
(* ++ str "in env:" ++ my_print_env env); *)
@@ -140,9 +140,15 @@ module Coercion = struct
let hdx = l.(i) and hdy = l'.(i) in
try isevars := the_conv_x_leq env hdx hdy !isevars;
let (n, eqT, restT) = destProd typ in
- aux (hdx :: tele) (subst1 hdy restT) (succ i) co
+ let (n', eqT', restT') = destProd typ' in
+ aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
with Reduction.NotConvertible ->
let (n, eqT, restT) = destProd typ in
+ let (n', eqT', restT') = destProd typ' in
+ let _ =
+ try isevars := the_conv_x_leq env eqT eqT' !isevars
+ with Reduction.NotConvertible -> raise NoSubtacCoercion
+ in
let restargs = lift_args 1
(List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
in
@@ -154,9 +160,9 @@ module Coercion = struct
let eq_app x = mkApp (Lazy.force eq_rect,
[| eqT; hdx; pred; x; hdy; evar|]) in
(* trace (str"Inserting coercion at application"); *)
- aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
- else co
- in aux [] typ 0 (fun x -> x)
+ aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
+ else Some co
+ in aux [] typ typ' 0 (fun x -> x)
in
(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
(* str " to "++ my_print_constr env y *)
@@ -264,21 +270,22 @@ module Coercion = struct
else
if i = i' && len = Array.length l' then
let evm = evars_of !isevars in
- let typ = Typing.type_of env evm c in
(try subco ()
- with NoSubtacCoercion ->
-
-(* if not (is_arity env evm typ) then *)
- Some (coerce_application typ c c' l l'))
-(* else subco () *)
+ with NoSubtacCoercion ->
+ let typ = Typing.type_of env evm c in
+ let typ' = Typing.type_of env evm c' in
+ (* if not (is_arity env evm typ) then *)
+ coerce_application typ typ' c c' l l')
+ (* else subco () *)
else
subco ()
| x, y when x = y ->
if Array.length l = Array.length l' then
let evm = evars_of !isevars in
let lam_type = Typing.type_of env evm c in
+ let lam_type' = Typing.type_of env evm c' in
(* if not (is_arity env evm lam_type) then ( *)
- Some (coerce_application lam_type c c' l l')
+ coerce_application lam_type lam_type' c c' l l'
(* ) else subco () *)
else subco ()
| _ -> subco ())
diff --git a/lib/util.ml b/lib/util.ml
index c1cd93111..af99e2b23 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -350,7 +350,9 @@ let lowercase_utf8 s unicode =
| 0x038C -> 0x03CC
| x when 0x038E <= x & x <= 0x038F -> x + 63
| x when 0x0390 <= x & x <= 0x03AB & x <> 0x03A2 -> x + 32
- | x when 0x03AC <= x & x <= 0x039E ->
+ (* utf-8 Greek lowercase letters U03B0-03CE *)
+ | x when 0x03AC <= x & x <= 0x03CE -> x
+ | x when 0x03CF <= x & x <= 0x03FF ->
warning ("Unable to decide which lowercase letter to map to "^s); x
(* utf-8 Cyrillic letters U0400-0481 *)
| x when 0x0400 <= x & x <= 0x040F -> x + 80
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index be7b77ef0..0db172e82 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -17,9 +17,9 @@ Require Import ProofIrrelevance.
Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
Proof.
- intros n H.
- dependent destruction H.
- exists H ; exists a.
+ intros n v.
+ dependent destruction v.
+ exists v ; exists a.
reflexivity.
Save.
@@ -81,7 +81,7 @@ Qed.
Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
Proof with simpl in * ; simpl_depind ; auto.
intros until 1.
- dependent induction H generalizing Γ Δ α β...
+ dependent induction H generalizing Γ Δ α β.
destruct Δ...
apply weak ; apply ax.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 8e5729dce..34fff9d18 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1 as S1setoid.
-Instance DefaultRelation S1 eqS1.
+Instance eqS1_default : DefaultRelation S1 eqS1.
Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
-Instance DefaultRelation S1_test8 eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8.
Axiom f_test8 : S2 -> S1_test8.
Add Morphism f_test8 : f_compat_test8. Admitted.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 0f88fbdd9..b56ca26c3 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -45,6 +45,17 @@ Ltac simpl_one_dep_JMeq :=
Require Import Eqdep.
+(** Simplify dependent equality using sigmas to equality of the second projections if possible.
+ Uses UIP. *)
+
+Ltac simpl_existT :=
+ match goal with
+ [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
+ let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
+ end.
+
+Ltac simpl_existTs := repeat simpl_existT.
+
(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *)
Ltac elim_eq_rect :=
@@ -213,7 +224,8 @@ Ltac do_simpl_IHs_eqs :=
Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
-Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_IHs_eqs.
+Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
+ simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
(** The following tactics allow to do induction on an already instantiated inductive predicate
by first generalizing it and adding the proper equalities to the context, in a maner similar to
@@ -231,7 +243,7 @@ Ltac prepare_depind H :=
and starts a dependent induction using this tactic. *)
Ltac do_depind tac H :=
- prepare_depind H ; tac H ; simpl_depind.
+ prepare_depind H ; tac H ; repeat progress simpl_depind.
(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *)
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c9de1a9e1..d021326a1 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -13,16 +13,6 @@ Open Local Scope program_scope.
(** Tactics related to subsets and proof irrelevance. *)
-(** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
-
-Ltac simpl_existT :=
- match goal with
- [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
- let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
- end.
-
-Ltac simpl_existTs := repeat simpl_existT.
-
(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to
factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index cbc3b02ad..b6ba5d44e 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -50,9 +50,6 @@ Section Well_founded.
Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
Proof.
intro x; induction (Rwf x); intros.
- rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros.
- apply F_ext; auto.
- intros.
rewrite (proof_irrelevance (Acc R x) r s) ; auto.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 18:02:07 +0000