Logic_J.vより抜粋。tacticを使わずに証明オブジェクトを手書きするのを試しているけど僕には難しい。

andb_false.v

(*  **** Exercise: 1 star (bool_prop) *)
(** **** 練習問題: ★ (bool_prop) *)
Theorem andb_false : forall b c,
  andb b c = false -> b = false \/ c = false.
Proof.
  intros b c H.
  unfold andb in H.
  destruct b.
    right. apply H.
    left. reflexivity.
Qed.

Definition andb_false' : forall b c,
  andb b c = false -> b = false \/ c = false :=
  fun b c H =>
    match
      b
      return
      (match b with
       | true => c
       | false => false
       end = false -> b = false \/ c = false)
    with
    | true => fun H0 : c = false => or_intror (true = false) (c = false) H0
    | false => fun _ : false = false => or_introl (false = false) (c = false) eq_refl
    end H.

or_distributes_over_and.v

Theorem or_distributes_over_and_1 : forall P Q R : Prop,
  P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R).
Proof.
  intros P Q R. intros H. inversion H as [HP | [HQ HR]].
    Case "left". split.
      SCase "left". left. apply HP.
      SCase "right". left. apply HP.
    Case "right". split.
      SCase "left". right. apply HQ.
      SCase "right". right. apply HR.  Qed.

Definition or_distributes_over_and_1' : forall (P Q R : Prop),
  P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R) :=
    fun P Q R H =>
      match H with
      | or_introl HP =>
          conj (P \/ Q) (P \/ R) (or_introl P Q HP) (or_introl P R HP)
      | or_intror HQR =>
          match HQR with
          | conj HQ HR =>
              conj (P \/ Q) (P \/ R) (or_intror P Q HQ) (or_intror P R HR)
          end
      end.

(* and_ind : forall P Q P0 : Prop, (P -> Q -> P0) -> and P Q -> P0. *)

(*  **** Exercise: 2 stars, recommended (or_distributes_over_and_2) *)
(** **** 練習問題: ★★, recommended (or_distributes_over_and_2) *)
Theorem or_distributes_over_and_2 : forall P Q R : Prop,
  (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).
Proof.
  intros P Q R. intros H.
  inversion H as [ [HP0 | HQ] [HP1 | HR] ].
  left. apply HP0. (* HP0 HP1, P *)
  left. apply HP0. (* HP0 HR,  P *)
  left. apply HP1. (* HQ  HP1, P *)
  right. split.    (* HQ  HR,  Q /\ R *)
    apply HQ.      (* HQ  HR,  Q *)
    apply HR.      (* HQ  HR,  R *) 
Qed.

Definition or_distributes_over_and_2' : forall (P Q R : Prop),
  (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) :=
    fun P Q R H =>
      match H with
      | conj HPQ HPR' =>
          match HPQ with
          | or_introl HP0 =>
              fun HPR : P \/ R =>
                match HPR with
                | or_introl HP1 => or_introl P (Q /\ R) HP0
                | or_intror HR  => or_introl P (Q /\ R) HP0
                end
              (* fun _ : P \/ R => or_introl P (Q /\ R) HP0 *)
          | or_intror HQ =>
              fun HPR : P \/ R =>
                match HPR with
                | or_introl HP1 => or_introl P (Q /\ R) HP1
                | or_intror HR  => or_intror P (Q /\ R) (conj Q R HQ HR)
                end
          end HPR'
       end.

Definition or_distributes_over_and_2'' : forall (P Q R : Prop),
  (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) :=
    fun P Q R H =>
      match H with
      | conj HPQ HPR =>
          match HPQ with
          | or_introl HP0 => or_introl P (Q /\ R) HP0
          | or_intror HQ =>
              match HPR with
              | or_introl HP1 => or_introl P (Q /\ R) HP1
              | or_intror HR  => or_intror P (Q /\ R) (conj Q R HQ HR)
              end
          end
       end.

(** [] *)

(*  **** Exercise: 1 star (or_distributes_over_and) *)
(** **** 練習問題: ★ (or_distributes_over_and) *)
Theorem or_distributes_over_and : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  intros P Q R.
  split.
    apply or_distributes_over_and_1'.
    apply or_distributes_over_and_2''.
Qed.

Definition or_distributes_over_and' : forall P Q R,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) :=
  fun P Q R =>
    conj (P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R))
         ((P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R))
         (or_distributes_over_and_1' P Q R)
         (or_distributes_over_and_2' P Q R).
      
(** [] *)