(* ACM SAC 2016 - Tutorial *) (* http://frederic.loulergue.eu/sac2016 *) (* Frédéric Loulergue, Université d'Orléans *) (* * Statements of Theorems *) Lemma lemma1: forall (b:bool), negb(negb b) = b. Admitted. Check lemma1. (* * Inductive Predicates *) Inductive leq (n:nat) : nat -> Prop := | le_n : leq n n | le_S : forall m, leq n m -> leq n (S m). Check Prop. Check Set. Notation "n <= m" := (leq n m). (* * Simple proofs *) Lemma plus0n : forall n, 0 + n = n. Proof. intro n. reflexivity. Qed. Lemma negb_negb: forall (b:bool), negb(negb b) = b. Proof. intro b. destruct b. - simpl. reflexivity. - simpl. trivial. Qed. Lemma leq_n_Sn: forall n, n <= S n. Proof. intro n. apply le_S. apply le_n. Qed. (* * Inductive Proofs *) Lemma plusn0 : forall n, n + 0 = n. Proof. induction n as [ | n Hn ]. - reflexivity. - simpl. rewrite Hn. trivial. Qed. (* * Proofs as Arguments *) Require Import List. Import ListNotations. Fail Definition head A (xs: list A) (H: xs<> []) : A := match xs with | [] => _ | x::_ => x end. Definition head A (xs: list A) (H: xs<> []) : A. destruct xs. - contradict H. trivial. - exact a. Defined. Print head. Module WithProgram. Program Definition head A (xs:list A)(H: xs<>[]):A:= match xs with | [] => _ | x::_ => x end. End WithProgram. Require Import ExtrOcamlBasic. Recursive Extraction WithProgram.head. (* * Dependant Pairs *) Print sig. Module DependantPairs. Program Definition head A (xs:{l:list A|l<>[]}) :A:= match xs with | [] => _ | x::_ => x end. End DependantPairs. (* * Type Classes *) Generalizable All Variables. Class LeftNeutral `(op: B -> A -> A) (e : B) := { left_neutral : forall a, op e a = a }. Class RightNeutral `(op: A -> B -> A) (e : B) := { right_neutral : forall a, op a e = a }. Class Neutral `(op: A -> A -> A) (e : A) := { neutral_left_neutral :> LeftNeutral op e; neutral_right_neutral :> RightNeutral op e }. Class Associative `(op:A->A->A) := { associative : forall (x y z: A), op (op x y) z = op x (op y z) }. Class Monoid `(op : A->A->A) (e : A) := { monoid_assoc :> Associative op; monoid_neutral :> Neutral op e }. Require Import Arith. Program Instance plus_O_monoid : Monoid plus 0. Next Obligation. apply Build_Associative. intros x y z. now rewrite plus_assoc. Qed. Next Obligation. constructor. - constructor. trivial. - constructor. intros. now rewrite plus_n_O. Qed. Definition reduce `(op:A->A->A) `{Monoid A op e} (l:list A) : A := fold_left op l e. Definition result1 := reduce plus [0;1;2]. Eval compute in result1. (* = 3 : nat *) Require Import ZArith. Fail Definition resulte := reduce Zplus ([ -1; 0; 1 ])%Z. Print Instances Monoid. (* * Exercises *) (** * Properties of [fold_left] and [fold_right] *) Lemma fold_left_map_r: forall `(f:A->B->A) `(g :C->B) (l:list C) (a:A), fold_left (fun a b => f a (g b)) l a = fold_left f (map g l) a. Proof. (* To complete *) (* Suggested tactics : induction, intro, intros, rewrite, trivial *) Admitted. (* Do not forget to replace by Qed. *) Lemma fold_right_map_l: forall `(f:B->A->A)`(g:C->B) (l:list C) (a:A), fold_right (fun a b => f (g a) b) a l = fold_right f a (map g l). Proof. (* To complete *) (* Suggested tactics : induction, intro, rewrite, simpl, trivial *) Admitted. (* Do not forget to replace by Qed. *) (* Associativity as a proposition *) Definition assoc `(f:A->A->A) : Prop := forall x y z, f (f x y) z = f x (f y z). Lemma fold_left_prop : forall (A:Type) f, assoc f -> forall l (a b:A), fold_left f l (f a b) = f a (fold_left f l b). Proof. (* To complete *) (* Tactics and tacticals: induction, intro, simpl, rewrite (and rewrite <-), trivial, now *) Admitted. Lemma fold_right_prop : forall (A:Type) f, assoc f -> forall l (a b:A), fold_right f (f a b) l = f (fold_right f a l) b. Proof. (* To complete *) (* Tactics and tacticals: induction, intro, simpl, rewrite (and rewrite <-), trivial, now *) Admitted. (** Associativity as a type class. *) Lemma fold_left_prop' `{Associative A f} : forall l (a b:A), fold_left f l (f a b) = f a (fold_left f l b). Proof. (* To complete *) Admitted. Lemma fold_right_prop' `{Associative A f} : forall l a b, fold_right f (f a b) l = f (fold_right f a l) b. Proof. (* To complete *) Admitted. (** * An alternative induction principle *) Lemma joinlist_induction : forall A, forall P : list A -> Prop, (P nil) -> (forall a, P [a]) -> (forall x y , P x -> P y -> P (x++y)) -> forall l, P l. Proof. (* Suggested tactics: intro, induction, trivial, apply, replace *) Admitted. (** * Lists and concatenation form a monoid *) Program Instance list_app_monoid : Monoid (@app A) []. Next Obligation. (* To complete *) Admitted. Next Obligation. (* To complete *) Admitted. Definition result2 := reduce (@app Set) [[nat ; bool];[list nat]]. Eval compute in result2. (* = [nat; bool; list nat] : list Set *)