change the indent in example_delay.v and remove the lemma expE_aux

theories/applications/example_delay.v

@@ -20,9 +20,9 @@ Lemma eq_fact_factdelay : forall n m, factdelay (n, m) ≈ Ret (m * n`!).
 Proof.
 move => n.
 rewrite /factdelay.
-elim: n => [m | n IH m].
-- by rewrite fixpointE bindretf muln1.
-- by rewrite fixpointE bindretf/= IH mulnA.
+elim: n => [m | n IH m]; rewrite fixpointE bindretf/=.
+- by rewrite muln1.
+- by rewrite mulnA.
 Qed.
 
 Let collatzm_body m n : M (nat + nat)%type :=
@@ -39,9 +39,9 @@ Proof.
 rewrite /collatzm /delaymul naturalityE.
 apply: whilewB => q.
 have [|] := eqVneq q 1 => Hs.
-  + by rewrite Hs bindretf/= fmapE bindretf/=.
-  + rewrite /collatzm_body !(ifN_eq _ _ Hs).
-    by have [|] := eqVneq (q %% 2) 0 => Hq; rewrite bindretf/= fmapE bindretf.
+  by rewrite Hs bindretf/= fmapE bindretf/=.
+rewrite /collatzm_body !(ifN_eq _ _ Hs).
+by have [|] := eqVneq (q %% 2) 0 => Hq; rewrite bindretf/= fmapE bindretf.
 Qed.
 
 Let minus1_body nm : M ((nat + nat * nat) + nat * nat)%type :=
@@ -71,9 +71,9 @@ Proof.
 rewrite /minus1 /minus2 -codiagonalE.
 apply: whilewB.
 move => [n m].
-  case: n => [|n /=].
-  + by case: m => //= [|n]; rewrite fmapE bindretf //.
-  + by rewrite fmapE bindretf.
+case: n => [|n /=].
+  by case: m => //= [|n]; rewrite fmapE bindretf //.
+by rewrite fmapE bindretf.
 Qed.
 
 Definition divide5_body (f : nat -> M nat) nm : M (nat + nat * nat)%type :=
@@ -105,28 +105,23 @@ Let fastexp_body nmk : M (nat + nat * nat * nat)%type :=
 
 Let fastexp n m k := while fastexp_body (n, m, k).
 
-Lemma expE_aux n : n <= n.*2.
-Proof.
-elim: n => //= n IH.
-rewrite doubleS ltnS.
-by apply (leq_trans IH (leqnSn _)).
-Qed.
-
 Lemma expE n: forall m k, fastexp n m k ≈ Ret (m * expn k n).
 Proof.
 rewrite /fastexp /fastexp_body.
 elim: n {-2}n (leqnn n) => n.
-- rewrite leqn0 => /eqP H0 m k.
+  rewrite leqn0 => /eqP H0 m k.
   by rewrite H0 fixpointE /= bindretf /= expn0 mulnS muln0 addn0.
-- move => IH [|m'] Hmn m k.
-  + by rewrite fixpointE /= bindretf /= mulnS muln0 addn0.
-  + case/boolP: (odd (m'.+1)) => Hm'.
-    * by rewrite fixpointE Hm' bindretf/= IH//= expnSr (mulnC (k^m') k) mulnA.
-    * rewrite fixpointE ifN //= bindretf /= IH.
-      ** by rewrite uphalfE mulnn -expnM mul2n (even_halfK Hm').
-      ** rewrite ltnS in Hmn.
-         rewrite leq_uphalf_double.
-         by apply (leq_trans Hmn (expE_aux _)).
+move => IH [|m'] Hmn m k.
+  by rewrite fixpointE /= bindretf /= mulnS muln0 addn0.
+case/boolP: (odd (m'.+1)) => Hm'.
+  by rewrite fixpointE Hm' bindretf/= IH//= expnSr (mulnC (k^m') k) mulnA.
+rewrite fixpointE ifN //= bindretf /= IH.
+  by rewrite uphalfE mulnn -expnM mul2n (even_halfK Hm').
+rewrite ltnS in Hmn.
+rewrite leq_uphalf_double.
+apply: (leq_trans Hmn).
+rewrite -addnn.
+by apply: leq_addr.
 Qed.
 
 Let mc91_body nm : M (nat + nat * nat)%type :=
@@ -153,54 +148,54 @@ Lemma mc91E_aux m n : 90 <= m <= 101 -> mc91 n m ≈ mc91 n 101.
 Proof.
 move => /andP [Hmin Hmax].
 case/boolP: (m < 101).
-- move/ltnW/subnKC.
+  move/ltnW/subnKC.
   set k:= 101 - m.
   clearbody k.
   move: m Hmin Hmax.
   elim: k.
-  + move => m Hmin Hmax.
+    move => m Hmin Hmax.
     by rewrite addn0 => ->.
-  + move => l IH m Hmin.
-    rewrite leq_eqVlt => /orP [/eqP H101 | Hm].
-    * by rewrite H101 => _.
-    * rewrite -addn1 (addnC l 1) addnA mc91succE ?Hmin // addn1.
-      apply IH => //.
-      by apply: leq_trans.
-- rewrite -leqNgt => H100.
-  have -> //: m = 101.
-  apply anti_leq => //.
-  by rewrite Hmax.
+  move => l IH m Hmin.
+  rewrite leq_eqVlt => /orP [/eqP H101 | Hm].
+    by rewrite H101 => _.
+  rewrite -addn1 (addnC l 1) addnA mc91succE ?Hmin // addn1.
+  apply IH => //.
+  by apply: leq_trans.
+rewrite -leqNgt => H100.
+have -> //: m = 101.
+apply anti_leq => //.
+by rewrite Hmax.
 Qed.
 
 Lemma mc91_101E n : mc91 n 101 ≈ Ret 91.
 Proof.
 elim: n => [|n IH]; rewrite/mc91/mc91_body fixpointE bindretf/=.
-- by rewrite fixpointE bindretf.
-- by rewrite -/mc91_body // -/(mc91 n 91) mc91E_aux // IH.
+  by rewrite fixpointE bindretf.
+by rewrite -/mc91_body // -/(mc91 n 91) mc91E_aux // IH.
 Qed.
 
 Lemma mc91E n m : m <= 101 -> mc91 n m ≈ Ret 91.
 Proof.
 move => H101.
 case/boolP: (90 <= m).
-- move => H89.
+  move => H89.
   move: (conj H89 H101) => /andP Hm.
   by rewrite mc91E_aux // mc91_101E.
-- rewrite -leqNgt -ltnS.
-  move/ltnW/subnKC.
-  set k:= 90 - m.
-  clearbody k.
-  elim: k {-2}k (leqnn k) n m {H101} => k.
-  + rewrite leqn0 => /eqP H0 n m.
-    rewrite H0 (addn0 m) => ->.
-    by rewrite mc91E_aux// mc91_101E.
-  + move =>IH k' Hk n m Hm.
-    have ->: m = 90 - k' by rewrite -Hm addnK.
-    rewrite/mc91/mc91_body fixpointE //=.
-    rewrite ifF; last by rewrite ltn_subRL addnC.
-    rewrite bindretf/= -/mc91_body -/(mc91 _ _).
-    case/boolP: (k' <= 11) => Hk'.
-      * rewrite mc91E_aux ?mc91_101E//; lia.
-      * rewrite -ltnNge in Hk'.
-        by rewrite (IH (k' - 11))//; lia.
+rewrite -leqNgt -ltnS.
+move/ltnW/subnKC.
+set k:= 90 - m.
+clearbody k.
+elim: k {-2}k (leqnn k) n m {H101} => k.
+  rewrite leqn0 => /eqP H0 n m.
+  rewrite H0 (addn0 m) => ->.
+  by rewrite mc91E_aux// mc91_101E.
+move =>IH k' Hk n m Hm.
+have ->: m = 90 - k' by rewrite -Hm addnK.
+rewrite/mc91/mc91_body fixpointE //=.
+rewrite ifF; last by rewrite ltn_subRL addnC.
+rewrite bindretf/= -/mc91_body -/(mc91 _ _).
+case/boolP: (k' <= 11) => Hk'.
+  by rewrite mc91E_aux ?mc91_101E//; lia.
+rewrite -ltnNge in Hk'.
+by rewrite (IH (k' - 11))//; lia.
 Qed.