Skip to content

Commit

Permalink
replace the tactics case: _ < _ for have [|] := ltnP _ _
Browse files Browse the repository at this point in the history
  • Loading branch information
@Ryuji-Kawakami
Ryuji-Kawakami committed Jan 9, 2025
1 parent 56d0f75 commit 488f345
Show file tree
Hide file tree
Showing 3 changed files with 91 additions and 117 deletions.
20 changes: 9 additions & 11 deletions theories/applications/example_delay.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ Proof.
move => n.
rewrite /factdelay.
elim: n => [m | n IH m]; rewrite fixpointE bindretf/=.
- by rewrite muln1.
- by rewrite mulnA.
by rewrite muln1.
by rewrite mulnA.
Qed.

Let collatzm_body m n : M (nat + nat)%type :=
Expand All @@ -38,10 +38,10 @@ Lemma collatzmwB m n p : delaymul p (collatzm m n) ≈ collatzm (p * m) n.
Proof.
rewrite /collatzm /delaymul naturalityE.
apply: whilewB => q.
have [|] := eqVneq q 1 => Hs.
have [Hs|Hns] := eqVneq q 1.
by rewrite Hs bindretf/= fmapE bindretf/=.
rewrite /collatzm_body !(ifN_eq _ _ Hs).
by have [|] := eqVneq (q %% 2) 0 => Hq; rewrite bindretf/= fmapE bindretf.
rewrite /collatzm_body !(ifN_eq _ _ Hns).
by have [|] := eqVneq (q %% 2) 0; rewrite bindretf/= fmapE bindretf.
Qed.

Let minus1_body nm : M ((nat + nat * nat) + nat * nat)%type :=
Expand Down Expand Up @@ -92,9 +92,9 @@ move => n.
rewrite /dividefac1 /dividefac2.
apply whilewB.
move => [k l].
have [|] := eqVneq (l %% 5) 0 => Hl/=.
- by rewrite Hl.
- by rewrite !(ifN_eq _ _ Hl) eq_fact_factdelay !bindretf mul1n.
have [Hl|Hln] := eqVneq (l %% 5) 0 => /=.
by rewrite Hl.
by rewrite !(ifN_eq _ _ Hln) eq_fact_factdelay !bindretf mul1n.
Qed.

Let fastexp_body nmk : M (nat + nat * nat * nat)%type :=
Expand Down Expand Up @@ -177,11 +177,9 @@ Qed.
Lemma mc91E n m : m <= 101 -> mc91 n m ≈ Ret 91.
Proof.
move => H101.
case/boolP: (90 <= m).
move => H89.
have [H89|] := leqP 90 m.
move: (conj H89 H101) => /andP Hm.
by rewrite mc91E_aux // mc91_101E.
rewrite -leqNgt -ltnS.
move/ltnW/subnKC.
set k:= 90 - m.
clearbody k.
Expand Down
161 changes: 69 additions & 92 deletions theories/applications/example_delayexcept.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,70 +8,61 @@ Section delayexcept_example.

Variable M : delayExceptMonad.

Definition select (l : seq nat) := let max := \max_(i <- l) i in (max, rem max l).
Definition select l := let max := \max_(i <- l) i in (max, rem max l).

Definition muloflistover10d_body (ln : (seq nat) * nat) : M (nat + (seq nat) * nat)%type :=
Definition muloflistover10d_body ln : M (nat + (seq nat) * nat)%type :=
match ln with (l, n) =>
match l with
|[::] => @ret M _ (inl n)
|h::tl => let (m,res) := select l in catch (if m <= 10 then fail else @ret M _ (inr (res, m*n))) (@ret M _ (inl n))
end
end.
|[::] => Ret (inl n)
|h::tl => let (m, res) := select l in catch (if m <= 10 then fail else Ret (inr (res, m * n))) (Ret (inl n))
end
end.

Definition muloflistover10d := while muloflistover10d_body.

Definition muloflistover10 (l : seq nat) := foldr (fun x z => if 10 < x then x*z else z) 1 l.
Definition muloflistover10 l := foldr (fun x z => if 10 < x then x * z else z) 1 l.

Lemma all_under10 (l : seq nat) : (forall i, i \in l -> i <= 10) -> muloflistover10 l = 1.
Lemma all_under10 l : (forall i, i \in l -> i <= 10) -> muloflistover10 l = 1.
Proof.
elim: l => //= n l' Hl H.
case/boolP: (10 < n) => H10.
- contradict H10.
have [H10|_] := ltnP 10 n.
contradict H10.
apply/negP.
rewrite -leqNgt.
apply H.
rewrite in_cons.
apply /orP.
left.
by apply/eqP.
- apply Hl.
move => m Hl'.
apply H.
rewrite in_cons.
apply/orP.
by right.
by rewrite in_cons eq_refl.
apply Hl => m Hl'.
apply H.
by rewrite in_cons Hl' orbT.
Qed.

Lemma muloflistover10_aux(l : seq nat) (k : nat): 10 < k -> k \in l -> k * muloflistover10 (rem k l) = muloflistover10 l.
move => Hk Hink.
rewrite/muloflistover10.
elim: l Hink => //= n l' IH Hink.
have [|] := eqVneq n k => [Hnk|/negPf Hnk].
- case/boolP: (10 < n) => Hn10.
+ by rewrite Hnk.
+ contradict Hk.
rewrite -Hnk.
by apply/negP.
- have Hkl': k \in l'.
move: Hink.
by rewrite in_cons eq_sym Hnk/=.
case/boolP : (10 < n) => Hn.
+ rewrite -(IH Hkl')/= Hn.
by rewrite mulnA (mulnC k n) -mulnA.
+ by rewrite -(IH Hkl')/= (ifN _ _ Hn).
have [Hnk|/negPf Hnk] := eqVneq n k.
have [|?] := ltnP 10 n.
by rewrite Hnk.
contradict Hk.
rewrite -Hnk.
apply/negP.
by rewrite -ltnNge.
have Hkl': k \in l'.
move: Hink.
by rewrite in_cons eq_sym Hnk/=.
have [Hn|HnN] := ltnP 10 n.
rewrite -(IH Hkl')/= Hn.
by rewrite mulnA (mulnC k n) -mulnA.
by rewrite -(IH Hkl')/= ltnNge HnN/=.
Qed.

Lemma maxinseq (l : seq nat): ~~(nilp l) -> \max_(i <- l) i \in l.
Proof.
move => Hn.
rewrite -(in_tupleE l).
rewrite big_tuple.
case: (eq_bigmax (tnth (in_tuple l))).
- rewrite cardT.
rewrite size_enum_ord.
rewrite lt0n. done.
- move => x ->.
by rewrite mem_tnth.
rewrite -(in_tupleE l) big_tuple.
case: (eq_bigmax (tnth (in_tuple l))) => [|x ->].
by rewrite cardT size_enum_ord lt0n.
by rewrite mem_tnth.
Qed.

Lemma muloflistover10E (l : seq nat) (n : nat) : muloflistover10d (l, n) ≈ Ret (n * (muloflistover10 l)).
Expand All @@ -81,55 +72,41 @@ move: n.
elim: len l Hlen.
- move => l /eqP/nilP Hl n.
by rewrite/muloflistover10/muloflistover10d/muloflistover10d_body Hl /= fixpointE /= bindretf /= mulnS muln0 addn0.
- move => m IH l' Hs n.
rewrite/muloflistover10d/muloflistover10d_body fixpointE /=.
elim: l' Hs => //= [h l''] _ Hs.
case: Hs => Hs.
case/boolP: (\max_(i <- (h :: l'')) i <= 10) => [/bigmax_leqP_seq Hm10|Hm10].
+ rewrite catchfailm.
rewrite bindretf /=.
have -> : (10 < h) = false.
apply/negP.
apply/negP.
rewrite -leqNgt.
apply Hm10 => //=.
rewrite in_cons.
by rewrite eq_refl.
rewrite all_under10.
* by rewrite mulnS muln0 addn0.
* move => i Hini.
apply Hm10 => //=.
rewrite in_cons.
by rewrite Hini orbT.
rewrite catchret bindretf /=.
rewrite -/muloflistover10d_body -/muloflistover10d.
have [Ht|Hf] := eqVneq h (\max_(i <- (h :: l'')) i).
* move: Hm10.
rewrite -Ht -ltnNge => Hm10.
by rewrite (IH l'' Hs) (ifT _ _ Hm10) (mulnC h n) mulnA.
* move: Hm10.
set k := \max_(i <- (h :: l'')) i.
have Hmaxin: k \in (h :: l'').
subst k.
by apply maxinseq.
rewrite IH/=.
** rewrite -ltnNge /= (mulnC k n) -mulnA.
have -> : (k * (if 10 < h then h * muloflistover10 (rem k l'') else muloflistover10 (rem k l''))) = ((if 10 < h then h * (k * muloflistover10 (rem k l'')) else k * muloflistover10 (rem k l''))).
case/boolP : (10 < h) => Hh10 //=.
by rewrite mulnA (mulnC k h) -mulnA.
move => Hk.
rewrite (muloflistover10_aux _ _ Hk) /=.
*** by [].
*** move: Hmaxin.
rewrite in_cons.
subst k.
by rewrite eq_sym (negPf Hf) /=.
** subst k.
rewrite /= size_rem.
*** case: l'' Hs Hf Hmaxin => [? contr|h' l''' Hs ? ?].
**** contradict contr.
by rewrite big_cons big_nil maxn0 eq_refl.
**** by rewrite prednK //=.
*** move: Hmaxin.
by rewrite in_cons eq_sym (negPf Hf) /=.
move => m IH l' Hs n.
rewrite/muloflistover10d/muloflistover10d_body fixpointE /=.
elim: l' Hs => //= [h l''] _ Hs.
case: Hs => Hs.
have [/bigmax_leqP_seq Hm10|Hm10] := leqP (\max_(i <- (h :: l'')) i) 10.
rewrite catchfailm bindretf /=.
have -> : (10 < h) = false.
apply/negP/negP.
rewrite -leqNgt.
apply Hm10 => //=.
by rewrite in_cons eq_refl.
rewrite all_under10.
by rewrite mulnS muln0 addn0.
move => i Hini.
apply Hm10 => //=.
by rewrite in_cons Hini orbT.
rewrite catchret bindretf /=.
rewrite -/muloflistover10d_body -/muloflistover10d.
have [Ht|Hf] := eqVneq h (\max_(i <- (h :: l'')) i).
by rewrite {2}Ht (ifT _ _ Hm10) (IH l'' Hs) -Ht (mulnC h n) mulnA.
move: Hm10.
set k := \max_(i <- (h :: l'')) i => Hk.
have Hmaxin : k \in (h :: l'').
subst k.
by apply maxinseq.
rewrite IH/=.
rewrite /= (mulnC k n) -mulnA fun_if.
rewrite (mulnA k h _) (mulnC k h) -mulnA (muloflistover10_aux _ _ Hk) //.
by move: Hmaxin; rewrite in_cons eq_sym (negPf Hf) /=.
subst k.
rewrite size_rem.
case: l'' Hs Hf Hk Hmaxin => [? contr|h' l''' Hs ? ?].
contradict contr.
by rewrite big_cons big_nil maxn0 eq_refl.
by rewrite prednK //=.
move: Hmaxin.
by rewrite in_cons eq_sym (negPf Hf) /=.
Qed.
27 changes: 13 additions & 14 deletions theories/applications/example_delaystate.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ Definition collatzs1_body nml : M ((nat * nat + nat * nat * nat) + nat * nat * n
do s' <- get;
do _ <- put (n :: s');
if n == 1 then if (l %% 4 == 1)
then Ret (inl (inl (m,l)))
then Ret (inl (inl (m, l)))
else do _ <- put [::]; Ret (inl (inr (m.+1, m.+1, 0)))
else if (n %% 2 == 0) then Ret (inr (n./2, m, l.+1))
else Ret (inr ((3 * n).+1, m, l.+1))
Expand All @@ -73,19 +73,18 @@ rewrite/collatzs1/collatzs2 -codiagonalE.
apply whilewB.
move => [[n' m] l].
rewrite/collatzs1_body/collatzs2_body.
have [|] := eqVneq (l %% 4) 1 => Hl/=.
- have [|] := eqVneq n' 1 => Hn'/=.
+ rewrite Hl fmapE bindA.
have [Hl|?] := eqVneq (l %% 4) 1 => /=.
have [|] := eqVneq n' 1 => /=.
rewrite Hl fmapE bindA.
rewrite bindfwB//= => a.
by rewrite bindA bindretf/=.
+ have [|] := eqVneq (n' %% 2) 0 => He/=;
rewrite fmapE/= bindA bindfwB//= => a;
by rewrite bindA bindretf.
- have [|] := eqVneq n' 1 => Hn' //=.
+ rewrite ifN //= fmapE bindA.
rewrite bindfwB //= => a.
by rewrite bindA bindA bindretf.
+ have [|] := eqVneq (n' %% 2) 0 => He/=;
rewrite fmapE/= bindA bindfwB//= => a;
by rewrite bindA bindretf.
have [|] := eqVneq (n' %% 2) 0 => /=;
rewrite fmapE/= bindA bindfwB//= => a;
by rewrite bindA bindretf.
have [Hn'|_] := eqVneq n' 1 => /=.
rewrite Hn' ifN //= fmapE bindA.
by under eq_bind do rewrite bindA bindA bindretf.
have [|] := eqVneq (n' %% 2) 0 => /=;
rewrite fmapE/= bindA bindfwB//= => a;
by rewrite bindA bindretf.
Qed.

0 comments on commit 488f345

Please sign in to comment.