Skip to content

Instantly share code, notes, and snippets.

@mvaled

mvaled/impl.v

Created May 26, 2016 16:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mvaled/1284963f4f12fffe7c8854a97f766848 to your computer and use it in GitHub Desktop.
Save mvaled/1284963f4f12fffe7c8854a97f766848 to your computer and use it in GitHub Desktop.
Download ZIP
Proof that '(p -> q -> z) <-> ((p /\ q) -> z)'.
Raw
impl.v
Section ImplicationProof.
Variables p q z : Prop.
Lemma T1: (p -> q -> z) -> ((p /\ q) -> z).
intros L P.
elim P.
trivial.
Save.
Lemma T2: ((p /\ q) -> z) -> (p -> q -> z).
intros.
cut (p /\ q); [trivial | split; [trivial | trivial]].
Save.
Lemma ImplicationChain: (p -> q -> z) <-> ((p /\ q) -> z).
split; [apply T1 | apply T2].
Qed.
End ImplicationProof.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment