(* Eduardo Hermo Reyes *) (* Coq built-in Logic *) (* Example *) (* Coq's built-in logic is very small.We will see how to use some tactics to carry out standard forms of logical reasoning. *) Example E1 : forall A : Prop, A /\ ~ A -> False. Proof. intros. destruct H. apply H0. assumption. Qed. Check E1. Example E2: 0*3 = 0 /\ 1+1 = 2. Proof. split. reflexivity. reflexivity. Qed. (* In Coq a proposition P is inhabited by its proofs. We will refer to such inhabitants as proof term or proof object or evidence for the truth of P. *) Check forall A : Prop, A /\ ~ A -> False. Check E1. (* The proof term for an implication P → Q is a function that takes evidence for P as input and produces evidence for Q as its output. *) Example E3: forall A B : Prop, A -> A \/ B. Proof. intros. left. assumption. Qed. Print E3. Example Construct1: forall A : Prop, A -> ~~A. Proof. intros. intro. apply H0; assumption. Qed. Example Construct2: forall A : Prop, ~~~A -> ~A. Proof. intros. intro. apply H. apply Construct1; assumption. Qed. (* Example E4: forall A : Prop, ~~A -> A. Proof. intros. *) (* To prove a conjunction P /\ Q we must provide evidence for P and evidence for Q *) (* If conjunction is in our goals *) Example E4 : forall A B : Prop, A -> B -> A /\ B. Proof. intros. split. assumption. assumption. Qed. (* If conjunction is in our hypothesis *) Example E5: forall A B : Prop, A /\ B -> B. Proof. intros. destruct H. assumption. Qed. (* To prove a disjunction P \/ Q, we must provide an evidence for P and say that it is P you are giving evidence for, or an evidence for Q *) (* See Example E3 *) Example E6: forall A B : Prop, A \/ B -> B \/ A. Proof. intros. destruct H. right. assumption. left. assumption. Qed. (* Falsehood: False is a proposition for which there is no way to give evidence. Which are the inhabitants of False? *) Theorem False_implies_nonsense : False -> 2 + 2 = 5. Proof. intros. inversion H. Qed. Theorem Ex_Falso_Loquequieras : forall A : Prop, False -> A. Proof. intros. inversion H. Qed. (* inversion H breaks H nto each of its possible cases, and yields a subgoal for each case. However, False has no inhabitant, so therefore there possible subgoal *) (* We can use False and -> for negation. The intuition for ~P is that if we assume to have a proof of P then anything at all, even False, follows from that. *) Example E7: 2 + 2 <> 5. Proof. intro. inversion H. Qed. (* True is rarely used. The intuition is that is trivial to give an evidence *) Example E8 : forall A : Prop, A -> True. Proof. intros. trivial. Qed. Theorem T1 : ~ False <-> True. Proof. split. intro. trivial. intro. intro. inversion H0. (* / assumption *) Qed. Theorem T2 : ~~False <-> False. Proof. split. intro. apply H. apply T1. trivial. intro. intro. apply H0. assumption. Qed.