(* The way to interact with Coq through CoqIDE is by using the up and
   down arrow buttons at the top of the screen.  At any time, some
   fraction of the text has been introduced into Coq's brain, and the
   rest has not.  The part that Coq knows about is highlighted in
   color.  The down button adds the next command to Coq's brain, and
   the up button removes the previous one.

   Emacs ProofGeneral works the same way, except that there are key
   commands instead: [C-c C-n] to move forward, [C-c C-u] to go back.
   *)

(* We haven't seen how to define any numbers or arithmetic yet, but
   for purposes of these exercises, we suppose we have a type [nat]
   which contains the usual natural numbers and on which the usual
   arithmetic operations [+], [*], and [-] are defined.  (Such a type
   is predefined in Coq.) **)

(** Let's start by getting some practice defining terms and evaluating
   them in Coq. **)

Eval compute in (2+2).

(** One very important thing to notice is that every command to Coq
   ends with a period.  **)

(** Coq's [Definition] command allows us to assign a name to any term
   in the empty context (i.e. one without free variables). **)

Definition a := 15.
Check a.                        (* Prints the type of [a] *)
Print a.                        (* Prints the value of [a] and its type *)
Definition b := (2 * 13) - 4.

(** Observe that [b] is an expression, not a number, until we compute it. **)

Print b.
Eval compute in b.

(** Now let's define some functions.  Note that Coq's syntax for
   \lambda is [fun]. **)

Definition square := fun x => x * x.

Eval compute in (square(4)).

(** We can specify the type in any definition, too, if we want.  (If we
   don't specify it, Coq tries to guess.)  Note that Coq doesn't care
   about the presence or absence of line breaks. **)

Definition three_x_plus_one : nat -> nat
  := fun x => 3 * x + 1.

(** The way we define functions of more than one variable is to define
   one function which returns another function. **)

Definition two_x_plus_three_y : nat -> (nat -> nat)
  := fun x => (fun y => (2 * x) + (3 * y)).

Eval compute in (two_x_plus_three_y(4)(1)).

(** Because this is so common, Coq lets us omit the parentheses on the
   type, in the definition, and in the application. **)

Definition four_x_minus_y : nat -> nat -> nat
  := fun x => fun y => (4 * x) - y.

Eval compute in (four_x_minus_y 3 7).

(** An even easier shorthand for such a definition. **)

Definition x_times_y_squared : nat -> nat -> nat
  := fun x y => x * y * y.

(** Exercise 2.1: Define a function which takes three natural numbers,
   multiplies the first by the third, then adds the second.  Test it
   using [Eval compute]. **)

(* FILL IN HERE *)

(** Exercise 2.2: Without using the keyword [fun], define a function
   which takes one input, multiplies it by five, and adds two.  (Hint:
   use the previous exercise.) **)

(* FILL IN HERE *)

(** Exercise 2.3: Coq will not accept the following Definition.  Without
   trying to evaluate the definition, try to guess what is wrong with
   it, and what sort of error message Coq might give.  Then see
   whether you were right. **)

Definition identity := fun x => x.

(** Next, let's look at some positive type constructors, starting with
   the cartesian product. **)

Definition one_two : nat * nat := (1,2).

Print one_two.

Definition one_plus_two :=
  match one_two with
    | (x,y) => x + y
  end.

Eval compute in one_plus_two.

(** We want to write some more generic programs now.  Thus, rather
   than working only with functions defined on natural numbers, we'll
   pick some letters that denote arbitrary unspecified types
   (i.e. we extend the context by three variables of type [Type]). **)

Section SomeFunctions.
Context (A B C : Type).

(** Exercise 2.4: Define the following function which swaps the order
   of the elements of an ordered pair.  **)

Definition swap : (A * B) -> (B * A) := 

(** The first type constructor we talked about was function types.
   We've already defined some functions, but now let's do some
   "higher-order functions" that take other functions as input.  **)

Definition compose : (A -> B) -> (B -> C) -> (A -> C)
  := fun f g => (fun x => g (f x)).

(** Exercise 2.5: For each of the following types, define a term
   that has that type, if you can.  If you can, how many different
   things do you think can you define with that type?  If you can't
   define any, why not?  **)

Definition ex5a : A -> A -> A :=


Definition ex5b : (A -> A) -> (A -> A) :=


Definition ex5c : A :=


Definition ex5d : A -> B :=


Definition ex5e : B -> (A -> B) :=


(** Note that with ordered pairs, we have a different way to define a
   function of two variables. **)

Definition ten_x_minus_five_y : (nat*nat) -> nat
  := fun xy => match xy with
                 | (x,y) => (10 * x) - (5 * y)
               end.

(** Exercise 2.6: Define a higher-order function which, given a
   function of two variables defined in the first style we introduced,
   returns a version of the same function which accepts its two
   arguments as an ordered pair.  Then define a function which does
   the inverse translation. **)

Definition uncurry : (A -> B -> C) -> (A*B -> C) :=


Definition curry : (A*B -> C) -> (A -> B -> C) :=


(** The word "currying" for this operation is named after the
   mathematician Haskell Curry, who has the simultaneous and rare
   distinctions of having his last name turned into a verb and his
   first name given to a programming language. **)

(** The next type constructor is a disjoint union, written [A + B].
   There are two ways to construct an element of [A + B]: by
   "injecting" an element of [A], or injecting an element of [B]. **)

Definition left_two : nat + nat := inl _ 2.
Print left_two.

Definition left_two' := inl nat 2.
Print left_two'.

Definition right_two : nat + nat := inr _ 2.
Print right_two.

Definition right_two' := inr nat 2.
Print right_two'.

(* Note that if Coq allowed us to write simply [inl 2], that would be
   ambiguous: since [2] has type [nat], Coq can guess that the type of
   [inl 2] should be [nat + something], but it has no way to guess
   what the something is.  Thus [inl] takes a first argument
   specifying that something.  If the context does allow Coq to guess
   (such as if we've specified the type we want the overall expression
   to have), then we can write an underscore [_] to tell Coq "please
   guess what should go here".  *)

(** The way to extract the data that's been injected into a disjoint
   union is with a different version of [match].  Now we need two
   clauses, specifying what action to take depending on whether the
   input value came from the left copy or the right copy.

   Note that the first argument of [inl] and [inr] is *not* written
   when matching against them.  We'll see why this is later, when we
   discuss parameters and indices of inductive types. **)

Definition addtwo_or_subtractone : nat + nat -> nat
  := fun x_or_y => match x_or_y with
                     | inl x => x + 2
                     | inr y => y - 1
                   end.

Eval compute in (addtwo_or_subtractone (inl _ 5)).
Eval compute in (addtwo_or_subtractone (inr _ 5)).

(** Exercise 2.7: Define functions with the following types. **)

Definition ex7a : (A+B -> C) -> ((A -> C) * (B -> C)) :=


Definition ex7b : ((A -> C) * (B -> C)) -> (A+B -> C) :=


Definition ex7c : (A*(B+C)) -> (A*B + A*C) :=


Definition ex7d : (A*B + A*C) -> (A*(B+C)) := 


(** The type [unit] has exactly one element, called [tt]. **)

Check tt.

(** We can match against [tt], although it's kind of silly to do so. **)

Definition silly : unit -> nat
  := fun x => match x with
                | tt => 42
              end.

(** The type [Empty_set] has no elements at all, so when we match
   against it, we don't need to include any clauses at all. *)

Definition from_empty (p : Empty_set) : A
  := match p with
     end.

(** By the way, the command [Definition] works just as well to define
   a type, using type-operations like cartesian product and disjoint
   union.  However, we have to give Coq a little help to guess what we
   mean, since the symbols [+] and [*] also refer to the arithmetic
   operations. **)

Definition pair_of_nat_and_A := ( nat * A )%type.

(* The next command closes the scope of the [Context] declaration
   given above, so that we are no longer assuming three variables of
   type [Type]. *)

End SomeFunctions.

(* When we close the scope like this, Coq automatically performs a
   dependent lambda-abstraction on all the objects we defined inside
   the [Section], moving the [Context] variables into their types.
   You can see the result with: *)

Check swap.

(* The result is that now we can apply [swap] to arbitrary types [A]
   and [B], not just the particular ones we assumed when we were
   defining it.  But if that didn't make any sense, don't worry about
   it. *)


(** Next, we interpret all of the same constructions in terms of
   logic, using the propositions-as-type correspondence between

   - rules for how to prove or use logical propositions, and
   - rules for how to construct or destruct terms of certain types.

   Coq reifies this analogy by including logic into type theory,
   treating propositions as types, but with everything renamed.
   Whereas types are terms of type [Type], propositions are terms of
   type [Prop].  Moreover, all the type constructors have different
   names when we consider them acting on [Prop]; for instance, the
   cartesian product [A * B] becomes conjunction [P /\ Q].

   If you're going to use Coq for developing verified software or
   other traditional purposes, then you may want to learn to work with
   propositions in [Prop].  However, in homotopy type theory we don't
   use [Prop], so I won't be talking much about it.  Instead, the
   following exercises are all about types in [Type], but thought of
   as propositions rather than as types.  (This isn't what we do in
   homotopy type theory either, but it's fine for doing exercises.)

   I should mention that when actually working with Coq in practice,
   we use "tactic scripts" so that we don't have to write out proof
   terms by hand.  However, it's good to do a bit of the latter at the
   beginning, so that you understand what Coq is doing "under the
   hood".  Otherwise, tactics can feel like incomprehensible magic.

   Let's start out by assuming some arbitrary propositions. **)

Section SomePropositions.
Context (P Q R : Type).

(* This line tells Coq to make [*] and [+] refer to cartesian product
   and disjoint union by default, rather than multiplication and
   addition. *)
Open Scope type_scope.

(** Here is a proof that "and" distributes over "or". **)

Definition and_dist_or1 : P * (Q + R)  ->  (P * Q) + (P * R)
  := fun pqr => match pqr with
                  | (p,qr) => match qr with
                                | inl q => inl _ (p,q)
                                | inr r => inr _ (p,r)
                              end
                end.

(** Exercise 2.8: If you did exercise 7 above, this should look
   familiar.  What do the other parts of exercise 7 mean when
   interpreted propositionally? **)

(** Exercise 2.9: Prove that "or" distributes over "and".  What do
   these proofs mean as functions on types? **)

Definition or_dist_and1 :  P + (Q * R)  ->  (P + Q) * (P + R)
  :=


Definition or_dist_and2 : (P + Q) * (P + R)  ->  P + (Q * R)
  :=


(** Recall that the negation [not P] of a proposition [P] is defined
   to be [P -> Empty_set]. *)

Definition not (A : Type) := A -> Empty_set.

(* Using this definition, here is a proof of the double negation law. *)

Definition double_negation_1 : P -> not (not P)
  := fun p => fun notp => notp p.

(* Here is one direction of one of "de Morgan's laws".  **)

Definition demorgan_1a : not (P + Q) -> (not P * not Q)
  := fun notporq => (fun p => notporq (inl _ p),
                     fun q => notporq (inr _ q)).

(** And here is one direction of the law of the contrapositive. *)

Definition contrapositive_1 : (P -> Q) -> (not Q -> not P)
  := fun pimpq => fun notq => fun p => notq (pimpq p).

(** Exercise 2.10: Try to define terms which prove the following
   theorems.  Two are possible; one is not. **)

Definition demorgan_1b : (not P * not Q) -> not (P + Q)
  := 


Definition demorgan_2a : not (P * Q) -> (not P + not Q) 
  := 


Definition demorgan_2b : (not P + not Q) -> not (P * Q)
  := 


(** Recall that the proofs-as-programs logic is naturally
   "constructive".  In particular, this means that [P + not P] is not
   provable, since there is no _constructive_ or _computable_ way to
   decide which of [P] and [not P] should be true.  If we want [P + not P]
   to be true, however, we can simply add it as an axiom.
   *)

Section AssumeLEM.
Context (LEM : forall (R : Type), R + not R).

(* Important Note: this is not really the right formulation of LEM.
   Unless we really want to identify all types with propositions
   (which we don't in homotopy type theory), it's too strong to state
   it in this form.  But it will do for now, for practice.  **)

(* Now we can prove the other direction of the double negation law. *)

Definition double_negation_2 : not (not P) -> P
  := fun notnotp => match (LEM P) with
                      | inl p => p
                      | inr notp => match notnotp (notp) with end
                    end.

(** Exercise 2.11: The following is also unprovable without [LEM].
   Prove it using [LEM]. **)

Definition contrapositive_2 : (not Q -> not P) -> (P -> Q)
  := 

(** Exercise 2.12: Define a term which proves the impossible part of
   exercise 2.10, now using [LEM]. **)

(* FILL IN HERE *)

End AssumeLEM.

(** Exercise 2.13: Define a term which proves the following theorem,
   WITHOUT using the axiom [LEM] (or any of the previous exercises
   which used [LEM]).

   If you do any exercise in this class, you should do this one!
   **)

Definition nnLEM : not (not (P + not P))
  :=


End SomePropositions.

(** We could also take double negation as an axiom. **)

Section AssumeDN.
Context (DN : forall R, not (not R) -> R).

(** Exercise 2.14: Using the axiom [DN], but not (of course) the axiom
   [LEM], prove LEM. **)

Definition lem_using_dn : forall P, P + not P
  :=

End AssumeDN.

(* Finally, let's have some exercises about quantifiers.  Recall that
   the syntax for these is [forall x:A, P x] and [{ x:A & P x }].  Since
   proofs of [forall x:A, P x] are functions, we introduce them with
   [fun] and eliminate them by applying them.

   For existential quantification, the constructor is called [existT]
   and we eliminate by matching.  The constructor [existT] takes three
   arguments: one is the proposition [fun x => P x] (otherwise Coq
   couldn't in general guess what that is), while the second and third
   are an [a:A] and a proof of [P a].  But just as for [inl] and
   [inr], the first argument is *not* written when performing a
   [match] operation.

   To illustrate these points, here is a proof of a familiar logical
   equivalence.  *)

Definition notexists1 : forall (A:Type) (P:A->Type),
  not { x : A & P x } -> forall x, not (P x)
  := fun A P notexists => fun x => fun px =>
    notexists (existT (fun x => P x) x px).

(* Note that for technical reasons, we really do have to write
   [fun x => P x] rather than just [P], although you might think that
   should mean the same thing.  This "bug" (called eta-conversion, or
   more precisely the lack of eta-conversion) will be removed in the
   next upcoming release of Coq.  Often, though, we can write an
   underscore as the first argument to [existT] and Coq will guess
   what we mean. *)

(* Here is the opposite implication to [notexists1].  *)

Definition notexists2 : forall (A:Type) (P:A->Type),
  (forall x, not (P x)) -> not { x : A & P x }
  := fun A P forallxnotp => fun existsxpx =>
    match existsxpx with
      | existT a pa => forallxnotp a pa
    end.

(** Exercise 2.15: Prove the following two theorems.  One of them
   requires the axiom [LEM], but the other one doesn't. **)

Section AssumeLEMAgain.
Context (LEM : forall (R : Type), R + not R).

Definition notforall1 : forall (A:Type) (P:A->Type),
  { x : A & not (P x) } -> not (forall x, P x)
  :=

Definition notforall2 : forall (A:Type) (P:A->Type),
  not (forall x, P x) -> { x : A & not (P x) }
  :=

End AssumeLEMAgain.