Get rid of minimize in rasimpl

TheoWinterhalter · Aug 5, 2024 · 1a09805 · 1a09805
1 parent 66cd741
commit 1a09805
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 29 deletions.
diff --git a/theories/Param.v b/theories/Param.v
@@ -4307,7 +4307,7 @@ Proof.
         }
         2:{ intros y ey. rewrite <- nth_error_skipn in ey. assumption. }
         rasimpl. eapply extRen_cterm. intro n.
-        rewrite pren_comp_S. rewrite pren_plus.
+        minimize. rewrite pren_comp_S. rewrite pren_plus.
         unfold vreg. lia.
     + eapply ccmeta_conv.
       * econstructor. eapply param_ctx_vpar. all: eassumption.
@@ -4319,12 +4319,12 @@ Proof.
         2:{ intros y ey. rewrite <- nth_error_skipn in ey. assumption. }
         destruct_ifs.
         -- rasimpl. f_equal.
-          ++ eapply extRen_cterm. intro. rasimpl.
+          ++ eapply extRen_cterm. intro. minimize.
             rewrite pren_comp_S. rewrite pren_plus.
             unfold vpar. unfold shift, funcomp. lia.
           ++ rewrite epm_lift_eq. cbn. f_equal. unfold vpar, vreg. lia.
         -- rasimpl. f_equal.
-          ++ eapply extRen_cterm. intro. rasimpl.
+          ++ eapply extRen_cterm. intro. minimize.
             rewrite pren_comp_S. rewrite pren_plus.
             unfold vpar. unfold shift, funcomp. lia.
           ++ rewrite epm_lift_eq. cbn. f_equal. unfold vpar, vreg. lia.

diff --git a/theories/autosubst/CCAST_rasimpl.v b/theories/autosubst/CCAST_rasimpl.v
@@ -410,10 +410,6 @@ Ltac quote_subst s :=
     let q := quote_subst s in
     let q' := quote_subst t in
     constr:(qsubst_comp q q')
-  | λ x, subst_cterm ?s (?t x) =>
-    let q := quote_subst s in
-    let q' := quote_subst t in
-    constr:(qsubst_comp q q')
   | funcomp (ren_cterm ?r) ?s =>
     let qr := quote_ren r in
     let qs := quote_subst s in
@@ -422,16 +418,19 @@ Ltac quote_subst s :=
     let qs := quote_subst s in
     let qr := quote_ren r in
     constr:(qsubst_compr qs qr)
-  | λ x, ?s (?r x) =>
-    let qs := quote_subst s in
-    let qr := quote_ren r in
-    constr:(qsubst_compr qs qr)
   | scons ?t ?s =>
     let qt := quote_cterm t in
     let q := quote_subst s in
     constr:(qsubst_cons qt q)
   | ids => constr:(qsubst_id)
   | cvar => constr:(qsubst_id)
+  (* Instead of minimize *)
+  | λ x, ?g (?f x) =>
+    let t := constr:(funcomp g f) in
+    quote_subst t
+  | λ x, ?f x =>
+    let t := constr:(f) in
+    quote_subst t
   | _ => constr:(qsubst_atom s)
   end
 

diff --git a/theories/autosubst/GAST_rasimpl.v b/theories/autosubst/GAST_rasimpl.v
@@ -410,10 +410,6 @@ Ltac quote_subst s :=
     let q := quote_subst s in
     let q' := quote_subst t in
     constr:(qsubst_comp q q')
-  | λ x, subst_term ?s (?t x) =>
-    let q := quote_subst s in
-    let q' := quote_subst t in
-    constr:(qsubst_comp q q')
   | funcomp (ren_term ?r) ?s =>
     let qr := quote_ren r in
     let qs := quote_subst s in
@@ -422,16 +418,19 @@ Ltac quote_subst s :=
     let qs := quote_subst s in
     let qr := quote_ren r in
     constr:(qsubst_compr qs qr)
-  | λ x, ?s (?r x) =>
-    let qs := quote_subst s in
-    let qr := quote_ren r in
-    constr:(qsubst_compr qs qr)
   | scons ?t ?s =>
     let qt := quote_term t in
     let q := quote_subst s in
     constr:(qsubst_cons qt q)
   | ids => constr:(qsubst_id)
   | var => constr:(qsubst_id)
+  (* Instead of minimize *)
+  | λ x, ?g (?f x) =>
+    let t := constr:(funcomp g f) in
+    quote_subst t
+  | λ x, ?f x =>
+    let t := constr:(f) in
+    quote_subst t
   | _ => constr:(qsubst_atom s)
   end
 

diff --git a/theories/autosubst/RAsimpl.v b/theories/autosubst/RAsimpl.v
@@ -196,10 +196,6 @@ Ltac quote_ren r :=
     let q := quote_ren r in
     let q' := quote_ren r' in
     constr:(qren_comp q q')
-  | λ x, ?r (?r' x) =>
-    let q := quote_ren r in
-    let q' := quote_ren r' in
-    constr:(qren_comp q q')
   | scons ?n ?r =>
     let qn := quote_nat n in
     let q := quote_ren r in
@@ -208,6 +204,13 @@ Ltac quote_ren r :=
   | λ x, x => constr:(qren_id)
   | shift => constr:(qren_shift)
   | S => constr:(qren_shift)
+  (* Instead of minimize *)
+  | λ x, ?g (?f x) =>
+    let t := constr:(funcomp g f) in
+    quote_ren t
+  | λ x, ?f x =>
+    let t := constr:(f) in
+    quote_ren t
   | _ => constr:(qren_atom r)
   end.
 
@@ -286,10 +289,8 @@ Ltac rasimpl'_outermost :=
 
 Ltac rasimpl :=
   aunfold ;
-  minimize ;
   repeat rasimpl' ;
-  repeat rasimpl'_outermost ;
-  minimize.
+  repeat rasimpl'_outermost.
 
 (* Taken from core.minimize *)
 Ltac minimize_in h :=
@@ -308,10 +309,8 @@ Ltac rasimpl'_outermost_in h :=
 
 Ltac rasimpl_in h :=
   aunfold in h ;
-  minimize in h ;
   repeat rasimpl'_in h ;
-  repeat rasimpl'_outermost_in h ;
-  minimize in h.
+  repeat rasimpl'_outermost_in h.
 
 Tactic Notation "rasimpl" "in" hyp(h) :=
   rasimpl_in h.