SHARE
TWEET

Untitled

a guest Apr 21st, 2017 49 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (* exercise 3.5 from Coq Art *)
  2.  
  3. Section section_for_cut_example.
  4.   Variables P Q R T : Prop.
  5.  
  6.   Hypotheses (H  : P -> Q)
  7.              (H0 : Q -> R)
  8.              (H1 : (P -> R) -> T -> Q)
  9.              (H2 : (P -> R) -> T).
  10.  
  11.   Theorem cut_example : Q.
  12.   Proof.
  13.     cut (P -> R).
  14.     intro H3.
  15.     apply H1; [assumption | apply H2; assumption].
  16.     intro H3; apply H0; apply H; assumption.
  17.   Qed.
  18.  
  19.   Theorem cut_example_without_cut : Q.
  20.   Proof.
  21.     apply H1.
  22.     intro H3; apply H0; apply H; assumption.
  23.     apply H2.
  24.     intro H3; apply H0; apply H; assumption.
  25.   Qed.
  26. End section_for_cut_example.
RAW Paste Data
Pastebin PRO Summer Special!
Get 40% OFF on Pastebin PRO accounts!
Top