(** * PaT: Propositions as Types *) (* TERSE: HIDEFROMHTML *) Require Export Coq.Arith.Arith. Require Export Coq.Bool.Bool. (* TERSE: /HIDEFROMHTML *) (* ###################################################### *) (** ** Products and conjuction *) (** The product type is standard. It is like the type (a,b) in Haskell. We already saw its definition in chapter Poly. *) Inductive Prod (A B : Type) : Type := | pair : A -> B -> Prod A B. (** We declare the type arguments to be implicit and introduce standard notation. *) Arguments pair {A} {B} _ _. Notation "( M , N )" := (pair M N). Notation "A * B" := (Prod A B) : type_scope. (** (The annotation [: type_scope] tells Coq that this abbreviation should only be used when parsing types. This avoids a clash with the multiplication symbol.) *) (** Product introduction corresponds to [pair], and product elimination corresponds to [fst] and [snd]. [[[ G |- M : A G |- N : B ------------------------ *-I G |- (M,N) : A * B G |- L : A * B ----------------- *-E1 G |- fst L : A G |- L : A * B ----------------- *-E2 G |- snd L : B pair : forall A B : Type, A -> B -> A * B fst : forall A B : Type, A * B -> A snd : forall A B : Type, A * B -> B ]]] *) Definition fst {A B : Type} (p : A * B) : A := (* *) match p with | (x, y) => x end. Definition snd {A B : Type} (p : A * B) : B := match p with | (x, y) => y end. Check pair. Check fst. Check snd. (** Conjunction is just like pairs, but the components have type Prop rather than type Type *) Module Conjunction. Inductive prodP (P Q : Prop) : Prop := | pairP : P -> Q -> prodP P Q. Arguments pairP {P} {Q} _ _. Notation "P /\ Q" := (prodP P Q) : type_scope. End Conjunction. (** Conjunction introduction corresponds to [split], and conjunction elimination corresponds to [destruct]. [[[ G |- P G |- Q ---------------- /\-I G |- P /\ Q G |- P /\ Q ----------- /\-E1 G |- P G |- P /\ Q ----------- /\-E2 G |- Q ]]] *) Theorem conjI : forall P Q : Prop, P -> Q -> P /\ Q. Proof. intros P Q p q. split. - apply p. - apply q. Qed. Theorem conjE1 : forall P Q : Prop, P /\ Q -> P. Proof. intros P Q HPQ. destruct HPQ as [HP HQ]. apply HP. Qed. Theorem conjE2 : forall P Q : Prop, P /\ Q -> Q. Proof. intros P Q HPQ. destruct HPQ as [HP HQ]. apply HQ. Qed. (* ###################################################### *) (** ** Unit and true *) (** Whenever you encounter a binary operator, you should ask, what is its unit? Examples: [[[ 1 * n = n (one is the unit of multiplication) 0 + n = n (zero is the unit of addition) True /\ P = P (true is the unit of conjunction) False \/ P = P (false is the unit of disjunction) ]]] *) (** The Unit type is the unit of the product type, and True is the unit of conjunction. *) (** The unit type is standard. It is like the type () in Haskell. *) Inductive Unit : Type := | unit : Unit. (** Unit introduction corresponds to [unit], and there is no unit elimination. [[[ ------------------------ Unit-I G |- unit : Unit ]]] *) (** [True] is just like [Unit], but the components have type Prop rather than type Type *) Module Truth. Inductive True : Prop := | I : True. End Truth. (** Truth introduction is trivial, and there is no truth elimination. [[[ ---------------- True-I G |- True ]]] *) Theorem trueI : True. Proof. apply I. Qed. (* ###################################################### *) (** ** Sums and disjuction *) (** The sum type is standard. It is like the type Either in Haskell. *) Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. (** We declare the type arguments to be implicit and introduce standard notation. *) Arguments inl {A} {B} _. Arguments inr {A} {B} _. Notation "A + B" := (sum A B) : type_scope. (** Sum introduction corresponds to [inl] and [inr], and product elimination corresponds to [match]. [[[ G |- M : A ------------------ +-I1 G |- inl M : A + B G |- N : B ------------------ +-I2 G |- inr N : A + B G |- L : A + B G, x : A |- M : C G, y : B |- N : C ------------------------ *-I G |- (match L with inl x => M inr y => N) : C inl : forall A B : Type, A -> A + B inr : forall A B : Type, B -> A + B out : forall A B C : Type, (A -> C) -> (B -> C) -> (A + B -> C) ]]] *) Definition out {A B C : Type} (f : A -> C) (g : B -> C) (s : A + B) : C := match s with | inl x => f x | inr y => g y end. Check inl. Check inr. Check out. (** Disjunction is just like sums, but the components have type Prop rather than type Type *) Module Disjunction. Inductive sumP (P Q : Prop) : Prop := | inlP : P -> sumP P Q | inrP : Q -> sumP P Q. Arguments inlP {P} {Q} _. Arguments inrP {P} {Q} _. Notation "P \/ Q" := (sumP P Q) : type_scope. End Disjunction. (** Disjunction introduction corresponds to [left] and [right], and disjunction elimination corresponds to [destruct] [[[ G |- P ----------- \/-I1 G |- P \/ Q G |- Q ----------- \/-I2 G |- P \/ Q G |- P \/ Q G, P |- R G, Q |- R --------- \/-E G |- R ]]] *) Theorem disjI1 : forall P Q : Prop, P -> P \/ Q. Proof. intros P Q HP. left. apply HP. Qed. Theorem disjI2 : forall P Q : Prop, Q -> P \/ Q. Proof. intros P Q HP. right. apply HP. Qed. Theorem disjE : forall P Q R : Prop, (P -> R) -> (Q -> R) -> (P \/ Q) -> R. Proof. intros P Q R HPR HQR HPQ. destruct HPQ as [HP | HQ]. - apply HPR. apply HP. - apply HQR. apply HQ. Qed. (* ###################################################### *) (** ** Empty type and False *) (** The empty type is the unit of the sum type, and False is the unit of disjunction. *) (** The empty type is standard. *) Inductive Empty : Type :=. (** There is no empty introduction, and empty elimination corresponds to match with no branches. [[[ G |- L : Empty ------------------------------- Empty-E G |- (match L with) : C ]]] *) (** [False] is just like [Empty], but the components have type Prop rather than type Type *) Module Falsity. Inductive False : Prop :=. End Falsity. (** There is no False introduction, and elimination corresponds to [destruct] with no branches. [[[ G |- False ---------------- False-E G |- R ]]] *) Theorem falseE : forall R : Prop, False -> R. Proof. intros R HFalse. destruct HFalse as []. Qed. (* ###################################################### *) (** ** Implication and Negation *) (** Function introduction and elimination. [[[ G, x : A |- N : B ----------------------------------------- ->I G |- (fun x : A => N) : A -> B G |- L : A -> B G |- M : A -------------------- -> E G |- (L M) : B ]]] *) (** Implication introduction and elimination. [[[ G, P |- Q ---------------- ->I G |- P -> Q G |- P -> Q G |- P --------------- ->E G |- Q ]]] *) (** Negation introduction and elimination. [[[ G, P |- False ---------------- ->I G |- ~ P G |- ~ P G |- P --------------- ->E G |- False ]]] *) (** We can define negation in terms of implication *) Module Negation. Definition not (P:Prop) := P -> False. Notation "~ P" := (not P) : type_scope. End Negation. (* ###################################################### *) (** ** Universals and existentials *) (** Universal introduction and elimination. G, x : A |- N : B ------------------------------------------ forall-I G |- (lambda x : A => N) : forall x : A, B G |- L : forall x : A, B G |- M : A ------------------------ forall-E G |- L M : B[x := L] G, x : A |- P -------------------- forall-I G |- forall x : A, P G |- forall x : A, P G |- M : A -------------------- forall-E G |- P[x := M] ]]] *) (** Existential introduction and elimination. G |- M : A G |- N : B[x := M] ---------------------------- exists-I G |- (M,N) : exists x : A, B G |- L : exists x : A, B G, x : A, y : B |- N : C ------------------------ exists-E G |- (match L with | (x,y) => N) : C G |- M : A G |- P[x := M] -------------------- exists-I G |- exists x : A, P G |- exists x : A, P G, x : A, P |- Q -------------------- exists-E G |- Q ]]] *) Theorem exI : forall (A : Type), forall (P : A -> Prop), forall (M : A), P M -> (exists x : A, P x). Proof. intros A P M HPM. exists M. apply HPM. Qed. Theorem exE : forall (A : Type), forall (P Q : Prop), (exists x : A, P) -> (forall x : A, P -> Q) -> Q. Proof. intros A P Q HxP HxPQ. destruct HxP as [x HP]. apply (HxPQ x). apply HP. Qed. (** FULL: 2017/10/05 10:32:18 *) (* HIDE *) (* Local Variables: fill-column: 70 End: *) (* /HIDE *)