例が複雑すぎてすみません。私は持っている
Lemma test : forall x y z : Prop,
(
(((x → (y ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
∧ (((y → (x ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
∧ ((y → (x ∨ z)) → (x ∨ (x → (y ∨ z))))
∧ ((x → (y ∨ z)) → (y ∨ (y → (x ∨ z))))
) → ((x → (y ∨ z)) → (y ∨ z)).
やっている
Proof.
intros.
destruct H.
destruct H1.
destruct H2.
pose proof (H3 H0).
与える
1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y ∨ (y → x ∨ z)
______________________________________(1/1)
y ∨ z
私はそれを行いdestruct H4.、これは
2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y ∨ z
______________________________________(2/2)
y ∨ z
私はまだ理解していません:なぜ2つの同一の目標?? 私はしleft.、取得します
2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y
______________________________________(2/2)
y ∨ z
そしてassumption.与える
1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y → x ∨ z
______________________________________(1/1)
y ∨ z
それからやって
pose proof (H3 H0).
destruct H5.
left.
assumption.
再び 2 つの同一の目標を紹介し、
1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4, H5 : y → x ∨ z
______________________________________(1/1)
y ∨ z
これは、以前の状態と同じですが、現在 2 つの同一の施設があることを除きy → x ∨ zます。
ハマった。明らかに私は何か間違ったことをしていますが、何ですか？