Require Import Lists.List. Import ListNotations. Require Import Basics. Module OptionPlayground. Inductive option (X:Type) : Type := | Some: X -> option X | None: option X. Arguments Some {X} _. Arguments None {X}. End OptionPlayground. Module More. (** [apply] allows us to reuse true statements. Things we've proven or things we have assumed as hypotheses *) Theorem silly1 : forall (m n o p : nat), n = m -> [n;o] = [n;p] -> [n;o] = [m;p]. Admitted. (** Coq will find values for variables so that things match. Called unification. *) Theorem silly2 : forall n m o p : nat, n = m -> (forall q r : nat, q=r -> [q;o] = [r;p]) -> [n;o] = [m;p]. Admitted. Theorem silly2a : forall (n m : nat), (n,n) = (m,m) -> (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) -> [n] = [m]. Admitted. Example trans_eq_example : forall(a b c d e f : nat), [a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f]. Admitted. Theorem trans_eq : forall (X:Type) (n m o : X), n = m -> m = o -> n = o. Admitted. Example trans_eq_example' : forall (a b c d e f : nat), [a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f]. Admitted. Definition minustwo(n:nat):nat := n-2. Example trans_eq_exercise : forall(n m o p : nat), m = (minustwo o) -> (n + p) = m -> (n + p) = (minustwo o). Admitted. (** [injection] takes advantage of the injective property of constructed types. Specifically, that parts of equal constructions are also equal. *) Theorem S_injective : forall(n m : nat), S n = S m -> n = m. Admitted. Theorem S_injective' : forall (n m:nat), S n = S m -> n = m. Admitted. Theorem injection_ex1 : forall(n m o : nat), [n; m] = [o; o] -> [n] = [m]. Admitted. Theorem injection_ex2 : forall(n m : nat), [n] = [m] -> n = m. Admitted. Example injection_ex3 : forall(X : Type) (x y z : X) (l j : list X), x :: y :: l = z :: j -> y :: l = x :: j -> x = y. Admitted. Theorem discriminate_ex1 : forall(n : nat), S n = O -> 2 + 2 = 5. Admitted. Theorem discriminate_ex2 : forall(n m : nat), false = true -> [n] = [m]. Admitted. Example discriminate_ex3 : forall(X : Type) (x y z : X) (l j : list X), x :: y :: l = [] -> x = z. Admitted. Theorem f_equal : forall(A B : Type) (f: A -> B) (x y: A), x = y -> f x = f y. Admitted. End More.