Skip to content

Instantly share code, notes, and snippets.

@moretea

moretea/2.3.11a.v

Created December 1, 2014 22:25
Show Gist options
  • Save moretea/446fa18e6e65e2ef04f1 to your computer and use it in GitHub Desktop.
Save moretea/446fa18e6e65e2ef04f1 to your computer and use it in GitHub Desktop.
Download ZIP
Logic and Modelling, werkcollege 11.
Raw
2.3.11a.v
(* Exercise 2.3.11a *)
Require Import ProofWeb.
Variables P : D -> Prop.
Variable R : D * D -> Prop.
Variable b : D.
Theorem pred_050 : P b -> all x, (x=b -> P x).
Proof.
Raw
2.3.11b.v
(* Exercise 2.3.11b *)
Require Import ProofWeb.
Variables P : D -> Prop.
Variable R : D * D -> Prop.
Variable b : D.
Theorem pred_050 : P b -> all x, all y, ( (P x /\ P y) -> x = y) -> all x, (( P x -> x = b) /\ (x = b -> P x)).
Proof.
Raw
2.3.11c.v
(* Exercise 2.3.11c *)
Require Import ProofWeb.
Variable H : D * D -> Prop.
Theorem pred_050 : (exi x, exi y, ( H(x,y) \/ H(y,x))) -> (~exi x, ( H(x, x))) -> exi x, exi y, ~(x = y).
Proof.
Raw
2.3.11d.v
Require Import ProofWeb.
Variable H : D * D -> Prop.
Variable P : D -> Prop.
Variable b : D.
Theorem pred_050 : all x, ((P(x) -> x=b) /\ (x = b -> P(x))) -> all x, all y, ((P(x) /\ P(y)) -> x = y).
Proof.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment