minor proof simplification (fundamental for affine)

logsem · Feb 1, 2024 · ddddc3f · ddddc3f
1 parent 3c34ea1
commit ddddc3f
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 38 deletions.
diff --git a/theories/examples/affine_lang/logrel1.v b/theories/examples/affine_lang/logrel1.v
@@ -816,26 +816,16 @@ Section logrel.
     ⊢ valid1 Ω (interp_expr _ e) τ.
   Proof.
     intros H.
-    induction H.
+    iStartProof.
+    iInduction H as [| | | | | | | | | |] "IH".
     - by iApply compat_var.
-    - iApply compat_lam;
-        iApply IHtyped.
-    - iApply (@compat_app S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply (@compat_pair S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply (@compat_destruct S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply compat_alloc;
-        iApply IHtyped.
-    - iApply (@compat_replace S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply compat_dealloc;
-        iApply IHtyped.
+    - by iApply compat_lam.
+    - by iApply (@compat_app S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply (@compat_pair S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply (@compat_destruct S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply compat_alloc.
+    - by iApply (@compat_replace S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply compat_dealloc.
     - by iApply compat_nat.
     - by iApply compat_bool.
     - by iApply compat_unit.

diff --git a/theories/examples/affine_lang/logrel2.v b/theories/examples/affine_lang/logrel2.v
@@ -452,28 +452,19 @@ Section glue.
     typed_glued Ω e τ →
     ⊢ valid2 Ω (interp_expr _ e) τ.
   Proof.
-    intros typed. induction typed; simpl.
+    intros typed.
+    iStartProof.
+    iInduction typed as [| | | | | | | | | | |] "IH".
     - iApply glue_to_affine_compatibility.
       by iApply fundamental.
     - by iApply compat_var.
-    - iApply compat_lam.
-      iApply IHtyped.
-    - iApply (@compat_app _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply (@compat_pair _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply (@compat_destruct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply compat_alloc.
-      iApply IHtyped.
-    - iApply (@compat_replace _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
-      + iApply IHtyped1.
-      + iApply IHtyped2.
-    - iApply compat_dealloc.
-      iApply IHtyped.
+    - by iApply compat_lam.
+    - by iApply (@compat_app _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply (@compat_pair _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply (@compat_destruct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply compat_alloc.
+    - by iApply (@compat_replace _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight).
+    - by iApply compat_dealloc.
     - by iApply compat_nat.
     - by iApply compat_bool.
     - by iApply compat_unit.