繰り返しを使うっぽい

9.v

Module Q41.

Ltac split_all := try (split; split_all).

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma baz :
  forall P Q R S T : Prop,
    R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T.
Proof.
  intros P Q R S T H0 H1 H2 H3 H4.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma quux :
  forall P Q : Type, P -> Q -> P * Q.
Proof.
  intros P Q H0 H1.
  split_all.
  - assumption.
  - assumption.
Qed.

Record foo := {
  x : (False -> False) /\ True /\ (False -> False);
  y : True;
  z : (False -> False) /\ True
}.

Lemma hogera : foo.
Proof.
  split_all.
  - intros H; exact H.
  - intros H; exact H.
  - intros H; exact H.
Qed.

End Q41.

Module Q42.
Require Import Arith.
Require Import Omega.
Require Import Recdef.

Function log(n:nat) {wf lt n} :=
  if le_lt_dec n 1 then
    0
  else
    S (log (Div2.div2 n)).
Proof.
* assert (forall n, Div2.div2 n <= Div2.div2 (S n)).
    fix IHn 1. destruct n.
    constructor.
    simpl. destruct n. simpl. constructor. constructor.
    apply le_n_S. apply IHn.
  intros. clear teq.
  induction n; inversion anonymous; subst; clear anonymous.
  - constructor.
  - apply IHn in H1. clear IHn. destruct n.
    + constructor.
    + simpl. apply lt_n_S. eapply le_lt_trans; [|apply H1]; clear H1. apply H.
* red in *. constructor.
  induction a; intros; inversion H; subst; clear H.
  - constructor. assumption.
  - apply IHa. assumption.
Qed.
End Q42.

Module Q43.
Ltac split_all := try (match goal with |- _ /\ _  => split end; split_all).

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma baz :
  forall P Q R S T : Prop,
    R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T.
Proof.
  intros P Q R S T H0 H1 H2 H3 H4.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma quux :
  forall P Q : Type, P -> Q -> P * Q.
Proof.
  intros P Q H0 H1.
  split_all.
  split.
  - assumption.
  - assumption.
Qed.

End Q43.

Module Q44.
Require Import Arith.
Require Import Omega.
Require Import Recdef.

Function log(n:nat) {wf lt n} :=
  if le_lt_dec n 1 then
    0
  else
    S (log (Div2.div2 n)).
Proof.
* assert (forall n, Div2.div2 n <= Div2.div2 (S n)).
    fix IHn 1. destruct n.
    constructor.
    simpl. destruct n. simpl. constructor. constructor.
    apply le_n_S. apply IHn.
  intros. clear teq.
  induction n; inversion anonymous; subst; clear anonymous.
  - constructor.
  - apply IHn in H1. clear IHn. destruct n.
    + constructor.
    + simpl. apply lt_n_S. eapply le_lt_trans; [|apply H1]; clear H1. apply H.
* red in *. constructor.
  induction a; intros; inversion H; subst; clear H.
  - constructor. assumption.
  - apply IHa. assumption.
Qed.
(* ここまでは課題42 *)

Fixpoint pow(n:nat) :=
  match n with
  | O => 1
  | S n' => 2 * pow n'
  end.

Lemma log_pow_lb: forall n, 1 <= n -> pow (log n) <= n.
Proof.
  intros n H.
  functional induction (log n).
  - cut (n = 1). intros; subst; constructor.
    apply le_antisym; assumption.
  - clear e H; simpl; rewrite plus_0_r.
    assert (1 <= Div2.div2 n).
      inversion _x; subst; clear _x. constructor.
      inversion H; subst. constructor. simpl; apply le_n_S; apply le_0_n.
    eapply le_trans.
    apply plus_le_compat; apply IHn0; apply H.
    clear IHn0 H _x. generalize dependent n.
    fix IHn 1; destruct n as [|[|n]]; intros.
    constructor. constructor; constructor.
    simpl; rewrite <- plus_n_Sm. apply le_n_S; apply le_n_S.
    apply IHn.
Qed.
End Q44.

Module Q45.
Require Import ZArith.
Local Open Scope Z_scope.

Inductive Collatz: Z -> Prop :=
| CollatzOne: Collatz 1
| CollatzEven: forall x, Collatz x -> Collatz (2*x)
| CollatzOdd: forall x, Collatz (3*x+2) -> Collatz (2*x+1).

Theorem Collatz_1000: forall x, 1 <= x <= 1000 -> Collatz x.
Proof.

Qed.
End Q45.