(*---------------------------------*) (* Vernacular Commands *) (*---------------------------------*) Check refl_equal. Check true. Check bool. Check True. Check Prop. Print refl_equal. Print true. Print bool. Print True. (*Print Prop. *) Search eq. Locate nat. (*---------------------------------*) (* My first Coq Proof *) (* with intro, apply, assumption *) (* using single steps *) (*---------------------------------*) (* Lemma my_first_coq_proof: (A -> B -> C) -> (A -> B) -> A -> C. *) Lemma my_first_coq_proof: forall A B C: Prop, (A -> B -> C) -> (A -> B) -> A -> C. Proof. intros A B C pABC pAB pA. apply pABC. assumption. apply pAB. assumption. Qed. Check my_first_coq_proof. Print my_first_coq_proof. (*---------------------------------*) (* My second Coq Proof *) (* with intro, apply, assumption *) (* using tacticals *) (*---------------------------------*) Lemma my_second_coq_proof: forall A B C: Prop, (A -> B -> C) -> (A -> B) -> A -> C. Proof. intros A B C pABC pAB pA; apply pABC; [idtac | apply pAB]; assumption. Save. (*---------------------------------*) (* Inductive definitions *) (* propositional logic *) (*---------------------------------*) Print True. Print true. Check nat. Print nat. Goal forall A B P: Prop, (A \/ B) -> (A->P) -> (B->P) -> P. Proof. intros A B P AorB AthenP BthenP. destruct AorB as [Aholds|Bholds]. apply AthenP. exact Aholds. apply BthenP. exact Bholds. Qed. Goal forall A B C: Prop, (A \/ B) \/ C -> A \/ (B \/ C). Proof. intros. destruct H. destruct H. Print or. apply or_introl. assumption. right. left. assumption. right; right; assumption. Qed. (*---------------------------------*) (* Inductive definitions *) (* with exists *) (*---------------------------------*) Inductive is_even : nat-> Prop := Zero_is_even : is_even O |Succ_even : forall n:nat, is_even n -> is_even (S(S n)). Check is_even_ind. Goal forall n:nat, is_even n -> (n=0) \/ (exists m, n=S (S m)). Proof. intros. inversion H. left. apply refl_equal. right. exists n0. apply refl_equal. Qed. (*---------------------------------*) (* Inductive definitions *) (* recursive definitions *) (*---------------------------------*) Goal forall x, x+1=1+x. Proof. induction x. rewrite <- plus_n_O. rewrite plus_O_n. apply refl_equal. simpl. rewrite IHx. simpl. apply refl_equal. Qed. (*---------------------------------*) (* Inductive definitions *) (* recursive definitions *) (*---------------------------------*) Inductive list : Set := Empty : list | Cons: nat -> list -> list. Inductive append : list -> list -> list -> Prop:= EmptyAppend: forall l2, (append Empty l2 l2) | ConsAppend: forall x1 l1 l2 res, (append l1 l2 res) -> (append (Cons x1 l1) l2 (Cons x1 res)). Inductive is_rev : list -> list -> Prop:= IsRevEmpty: (is_rev Empty Empty) |IsRevCons: forall x1 l1 l2 res, (is_rev l1 l2)-> (append l2 (Cons x1 Empty) res) -> (is_rev(Cons x1 l1) res). Goal forall l ll lll, (is_rev l ll) -> (is_rev ll lll) -> l=lll. (* Exercise ;-) *) Admitted. (*---------------------------------*) (* Inductive definitions *) (* dependent types *) (*---------------------------------*) Inductive listd : nat -> Prop := Emptyd : (listd O) | Consd: forall n: nat, nat -> (listd n) -> (listd (S n)). Inductive appendd : forall n m: nat, listd n -> listd m -> listd (n+m) -> Prop:= EmptyAppenddd: forall m, forall l2, (appendd O m Emptyd l2 l2) | ConsAppenddd: forall n m x1 l1 l2 res, (appendd n m l1 l2 res) -> (appendd (S n) m (Consd n x1 l1) l2 (Consd (n+m) x1 res)).