aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers')
-rw-r--r--src/Compilers/CommonSubexpressionEliminationWf.v4
-rw-r--r--src/Compilers/Equality.v4
-rw-r--r--src/Compilers/MapCastByDeBruijnInterp.v1
-rw-r--r--src/Compilers/MapCastByDeBruijnWf.v1
-rw-r--r--src/Compilers/Named/ContextProperties/NameUtil.v10
-rw-r--r--src/Compilers/Named/ContextProperties/Proper.v25
-rw-r--r--src/Compilers/Named/NameUtilProperties.v2
-rw-r--r--src/Compilers/TestCase.v6
-rw-r--r--src/Compilers/Z/ArithmeticSimplifierWf.v11
-rw-r--r--src/Compilers/Z/Bounds/Interpretation.v2
10 files changed, 39 insertions, 27 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v
index 76ed1fa96..8d7bf2727 100644
--- a/src/Compilers/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/CommonSubexpressionEliminationWf.v
@@ -99,7 +99,7 @@ Section symbolic.
: wff G' (@csef var1 t e1 m1) (@csef var2 t e2 m2).
Proof.
revert dependent m1; revert m2; revert dependent G'.
- induction Hwf; simpl; intros; try constructor; auto.
+ induction Hwf; simpl; intros G' HGG' m2 m1 Hlen Hm1m2None Hm1m2Some; try constructor; auto.
{ erewrite wff_norm_symbolize_exprf by eassumption.
break_innermost_match;
try match goal with
@@ -170,7 +170,7 @@ Section symbolic.
(Hwf : wff G e1 e2)
: wff G (@prepend_prefix var1' t e1 prefix1) (@prepend_prefix var2' t e2 prefix2).
Proof.
- revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros; try congruence.
+ revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros Hlen Hprefix G Hwf; try congruence.
{ pose proof (Hprefix 0) as H0; specialize (fun n => Hprefix (S n)).
destruct_head sigT; simpl in *.
specialize (H0 _ _ _ _ eq_refl eq_refl); destruct_head ex; subst; simpl in *.
diff --git a/src/Compilers/Equality.v b/src/Compilers/Equality.v
index 8e2b44de8..2b54a7892 100644
--- a/src/Compilers/Equality.v
+++ b/src/Compilers/Equality.v
@@ -51,7 +51,7 @@ Section language.
Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y.
Proof. clear base_type_code_lb; induction X, Y; t. Defined.
Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true.
- Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined.
+ Proof. clear base_type_code_bl; intros Y **; subst Y; induction X; t. Defined.
Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y}
:= match Sumbool.sumbool_of_bool (flat_type_beq X Y) with
| left pf => left (flat_type_dec_bl _ _ pf)
@@ -65,7 +65,7 @@ Section language.
Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y.
Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined.
Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true.
- Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined.
+ Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros Y **; subst Y; induction X; t. Defined.
Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y}
:= match Sumbool.sumbool_of_bool (type_beq X Y) with
| left pf => left (type_dec_bl _ _ pf)
diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v
index 10e09242a..7674e5f0e 100644
--- a/src/Compilers/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/MapCastByDeBruijnInterp.v
@@ -66,6 +66,7 @@ Section language.
then fun pf => left (base_type_code_bl_transparent _ _ pf)
else fun pf => right _) eq_refl).
{ clear -pf base_type_code_lb.
+ let pf := pf in
abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). }
Defined.
diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v
index 7c1e386b5..61a084ee7 100644
--- a/src/Compilers/MapCastByDeBruijnWf.v
+++ b/src/Compilers/MapCastByDeBruijnWf.v
@@ -64,6 +64,7 @@ Section language.
then fun pf => left (base_type_code_bl_transparent _ _ pf)
else fun pf => right _) eq_refl).
{ clear -pf base_type_code_lb.
+ let pf := pf in
abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). }
Defined.
diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v
index 0bc970357..320d910f0 100644
--- a/src/Compilers/Named/ContextProperties/NameUtil.v
+++ b/src/Compilers/Named/ContextProperties/NameUtil.v
@@ -47,7 +47,7 @@ Section with_context.
: (exists t, @find_Name n T N = Some t)
<-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls).
Proof using Type.
- revert dependent ls; intro ls; revert ls ls'; induction T; intros;
+ revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' H;
[ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls)));
specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
repeat first [ misc_oname_t_step
@@ -77,7 +77,11 @@ Section with_context.
rewrite fst_split_onames_firstn, snd_split_onames_skipn in H.
inversion_prod; subst.
split; [ split | intros [? ?] ]; eauto using In_firstn, oname_list_unique_specialize.
- eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto.
+ match goal with
+ | [ H : List.In (Some _) ?ls |- _ ]
+ => is_var ls;
+ eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto
+ end.
Qed.
Lemma split_onames_find_Name_Some_unique
@@ -97,7 +101,7 @@ Section with_context.
: @find_Name_and_val var' t n T N V None = Some v
<-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V).
Proof using Type.
- revert dependent ls; intro ls; revert ls ls'; induction T; intros;
+ revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' Hls H;
[ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls)));
specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
repeat first [ find_Name_and_val_default_to_None_step
diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v
index 48cecde8f..0c583e446 100644
--- a/src/Compilers/Named/ContextProperties/Proper.v
+++ b/src/Compilers/Named/ContextProperties/Proper.v
@@ -41,15 +41,15 @@ Section with_context.
| rewrite lookupb_removeb_different by assumption
| solve [ auto ] ].
- Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10.
+ Global Instance extendb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10.
Proof.
- intros ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'.
+ intros t ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'.
Qed.
- Global Instance removeb_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10.
+ Global Instance removeb_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10.
Proof.
- intros ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'.
+ intros t ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'.
Qed.
- Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
+ Global Instance lookupb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
Proof. repeat intro; subst; auto. Qed.
Local Ltac proper_t2 t :=
@@ -68,13 +68,14 @@ Section with_context.
first [ eapply IHt2; [ eapply IHt1 | .. ]; auto
| idtac ] ].
- Global Instance extend_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10.
- Proof. proper_t2 t. Qed.
- Global Instance remove_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10.
- Proof. proper_t2 t. Qed.
- Global Instance lookup_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10.
+ Global Instance extend_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10.
+ Proof. intro t; proper_t2 t. Qed.
+ Global Instance remove_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10.
+ Proof. intro t; proper_t2 t. Qed.
+
+ Global Instance lookup_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10.
Proof.
- proper_t2 t.
+ intro t; proper_t2 t.
repeat match goal with
| [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ]
=> let G' := context G[match lookup A ctx na, lookup B ctx nb with
@@ -88,7 +89,7 @@ Section with_context.
| _ => progress subst
| _ => progress inversion_option
| _ => reflexivity
- | [ H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ]
+ | [ IHt2 : Proper _ (lookup t2), H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ]
=> assert (x = y)
by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity));
clear H H'
diff --git a/src/Compilers/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v
index d2791a5ea..944d164f2 100644
--- a/src/Compilers/Named/NameUtilProperties.v
+++ b/src/Compilers/Named/NameUtilProperties.v
@@ -171,7 +171,7 @@ Section language.
(t : flat_type base_type_code) (ls : list Name)
: fst (split_names t ls) <> None <-> List.length ls >= count_pairs t.
Proof using Type.
- revert ls; induction t; intros;
+ revert ls; induction t; intros ls;
try solve [ destruct ls; simpl; intuition (omega || congruence) ].
repeat first [ progress simpl in *
| progress break_innermost_match_step
diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v
index 36774e4e3..e1fb0087a 100644
--- a/src/Compilers/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -212,17 +212,17 @@ Module bounds.
Definition add_bounded_pf (x y : bounded_pf) : bounded_pf.
Proof.
exists (map_bounded_f2 plus false (proj1_sig x) (proj1_sig y)).
- simpl; abstract (destruct x, y; simpl; omega).
+ simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega).
Defined.
Definition mul_bounded_pf (x y : bounded_pf) : bounded_pf.
Proof.
exists (map_bounded_f2 mult false (proj1_sig x) (proj1_sig y)).
- simpl; abstract (destruct x, y; simpl; nia).
+ simpl; let x := x in let y := y in abstract (destruct x, y; simpl; nia).
Defined.
Definition sub_bounded_pf (x y : bounded_pf) : bounded_pf.
Proof.
exists (map_bounded_f2 minus true (proj1_sig x) (proj1_sig y)).
- simpl; abstract (destruct x, y; simpl; omega).
+ simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega).
Defined.
Definition interp_base_type_bounds (v : base_type) : Type :=
match v with
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index ba5dd39cd..56dda81ab 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -115,7 +115,8 @@ Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2}
end.
Proof.
invert_one_expr e1; intros; break_innermost_match; intros;
- try invert_one_expr e2; intros;
+ try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+ invert_one_expr e2); intros;
repeat first [ fin_t
| progress simpl in *
| progress intros
@@ -157,7 +158,9 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _
end.
Proof.
invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
- try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
+ try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+ invert_one_expr e2);
+ intros; break_innermost_match; intros; try exact I;
repeat first [ pret_step
| pose_wff_base
| break_t_step
@@ -206,7 +209,9 @@ Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2
end.
Proof.
invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
- try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
+ try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+ invert_one_expr e2);
+ intros; break_innermost_match; intros; try exact I;
repeat first [ pret_step
| pose_wff_base
| pose_wff_prod
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index dc29fe654..882cbde3a 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -288,7 +288,7 @@ Module Import Bounds.
:= interp_flat_type_rel_pointwise (@is_bounded_by').
Local Arguments interp_base_type !_ / .
- Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10.
+ Global Instance dec_eq_interp_flat_type : forall {T}, DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10.
Proof.
induction T; destruct_head base_type; simpl; exact _.
Defined.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 09:42:13 +0000