(*************************************) (*** Functional programming in Coq ***) (* basic function *) Definition f : nat -> nat := fun x : nat => x + x . Eval compute in f 4. (* higher order function *) Definition g : (nat -> nat) -> nat := fun h : nat -> nat => h 10 . Check g. Check g f. Eval compute in g f. (* basic pair *) Definition pair3_4 : nat * nat := (3,4) . (* projection via pattern matching *) Definition proj3 : nat := match pair3_4 with | (a,b) => a end . Eval compute in proj3. (* binary function (pair argument) *) Definition boo : (nat -> nat) * nat -> nat := fun p : (nat->nat) * nat => match p with | (func, arg) => func arg end . Eval compute in boo (f, 5). (* binary function in "Curry" style *) Definition boo2 : (nat -> nat) -> nat -> nat := fun func : nat->nat => fun arg : nat => func arg . Eval compute in boo2 f 5. (* Function definition using conventional notation, without "lambdas" *) Definition boh (func : nat -> nat) (arg : nat) : nat := func arg . Check boh. Eval compute in boh f 5. (* Dependently typed function: one argument (A) is used to define the types of next arguments *) Definition bar (A : Type) (func : A -> nat) (arg : A) : nat := func arg . Check bar. (* A forall type (dependent product) appears! *) (* Note that the usual function type (nat -> nat) can be written as a special case of the dependent product *) Check (nat -> nat). Check (forall unusedVariable : nat, nat). (*************************************) (*** Theorem proving in Coq ***) Print and. (* (conj proof1 proof2) is the "pair" representing and proofs *) Definition and_commutative: forall (p q : Prop), p /\ q -> q /\ p := fun (p q : Prop) => fun (H : p /\ q) => (* this is a pair of proofs! *) match H with | conj proofP proofQ => conj proofQ proofP end . Print or. (* or_introl , or_intror *) Definition and_implies_or: forall (p q : Prop), p /\ q -> p \/ q := fun (p q : Prop) => fun (H : p /\ q) => (* this is a pair of proofs! *) match H with | conj proofP proofQ => or_introl proofP (* we do not need proofQ *) end . Definition or_p_p_implies_p: forall p:Prop, p \/ p -> p := fun p:Prop => fun H : p \/ p => (* this is an element of a disjoint union *) match H with | or_introl proofP => proofP | or_intror proofP => proofP end . Definition or_example: forall (p q : Prop), (p -> q) /\ (p \/ q) -> q := fun (p q : Prop) => fun H : (p -> q) /\ (p \/ q) => match H with | conj H1 H2 => (* H1 : p->q and H2 : p\/q *) match H2 with | or_introl proofP => H1 proofP (* : q *) | or_intror proofQ => proofQ (* : q *) end end . (* Proving via the corresponding lambda-term is hard... Tactics provide an easier way *) Lemma or_example_again1: forall (p q : Prop), (p -> q) /\ (p \/ q) -> q . Proof. refine (fun p q => _). (* _ is a hole, we will fill it later *) refine (fun H => _). refine (match H with | conj H1 H2 => _ end). refine (match H2 with | or_introl proofP => _ | or_intror proofQ => _ end). (* this has two holes, generating two subproofs *) refine (H1 _). refine proofP. (* end of first subproof *) refine proofQ. Qed. Print or_example_again1. (* print the whole lambda-term *) (* The refine tactic is OK, but higher level tactics can make this much simpler *) Lemma or_example_again2: forall (p q : Prop), (p -> q) /\ (p \/ q) -> q . Proof. intros. (* take all the hypotheses you can *) elim H. (* use the "and" hypothesis *) intros. elim H1. (* use the "or" hypothesis *) intros. apply H0. (* use an implication whose thesis is the current goal *) exact H2. (* prove the premise *) intros. exact H2. Qed. Print or_example_again2. (* the lambda-term is correct, but not very readable. It exploits the induction principles for and & or *) Check and_ind. Check or_ind. (* A property on natuals *) Definition positive : nat -> Prop := fun n:nat => n>0 . Lemma positive_example: positive 3 . Proof. unfold positive. (* expand the definition of "positive" *) auto. (* the auto tactic solves most basic proofs *) Qed. (*************************************) (*** Inductive definitions in Coq ***) (* list of natural numbers *) Inductive natList : Set := | emptyList : natList | cons : nat -> natList -> natList . Eval compute in cons 3 (cons 4 (cons 5 emptyList)). (* We get an induction principle on lists for free!! *) Check natList_ind. (* trees of natural numbers *) Inductive natTree : Set := | emptyTree : natTree | branch : nat -> natTree -> natTree -> natTree . Eval compute in branch 3 emptyTree (branch 4 (branch 5 emptyTree emptyTree) (branch 6 emptyTree emptyTree)). Check natTree_ind. (* Properties can be defined inductively, too! *) Inductive isEven : nat -> Prop := | even0 : isEven 0 | evenS : forall n, isEven n -> isEven (n+2) . (* .. and we get the induction principle back. *) Check isEven_ind. Require Plus. (* Import some lemmas on + *) Lemma isEven_example: forall n, isEven n -> isEven (n+4) . Proof. (* here we use more advanced tactics *) intros. induction H. simpl. apply (evenS 2). apply (evenS 0). apply even0. cut (n+2+4 = n+4+2). intro. rewrite H0. apply evenS. apply IHisEven. rewrite <- (Plus.plus_assoc n 2 4). (* + associativity *) rewrite <- (Plus.plus_assoc n 4 2). simpl. reflexivity. Qed. (* Huge lambda-term *) Print isEven_example. (* A weird property ... *) Inductive strange : nat -> Prop := | strange0 : strange 0 | strangeS : forall n, strange (n+2) -> strange n . Check strange_ind. Lemma strange_only_0: forall n, strange n -> n=0 . Proof. intros. induction H. reflexivity. rewrite Plus.plus_comm in IHstrange. inversion IHstrange. Qed. Print strange_only_0.