Skip to content

Instantly share code, notes, and snippets.

@yuga

yuga/andb_false.v

Last active Aug 29, 2015
Embed
What would you like to do?
Logic_J.vより抜粋。tacticを使わずに証明オブジェクトを手書きするのを試しているけど僕には難しい。
(* **** 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.
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).
(** [] *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment