L02_Intro.v

(**
In Racket, we've now seen some very simple
expressions and even functions. The first
thing we saw was the expression (+ 3 4).
Let's pull this apart.
*)

(**
First, there are two values in there. In
type theory, every value has a type. The
Racket language implements an untyped (or
more accurately a single-typed) language.
Languages like Haskell and OCaml make the
types of values and expressions explicit.
We can "check" the type of a value of an
expression in Coq using "Check". (Capital
C, period at the end.)
*)

Check 3.
Check 4.

(**
Cool. So 3 is of type [nat], in Coq, the 
type of natural numbers, and so is 4. ...

But what is [nat]? In type theory, types
are a kind of value, too. So does [nat] 
have a type? Let's "Check."
*)

Check nat.
Check Set.

Check Type.

(**
Yes it does. The type of [nat] in Coq is
[Set]. [Set] is the type of computational
"things" in Coq, including data types, such
as [nat], and function types, which we'll
see a little later on.
*)

(**
How about "variables"? Can we declare a 
"variable" and tell Coq what type of value
it can be bound to? Sure. Here's an example.
*)

Definition aNum: nat.

(**
There are two things to think about now.

First, every expression has a type, and
now that we've declared [aNum] to be a
an expression, we expect it to have one.
What is the type of [aNum]?
*)

(**
Oops! Coq hasn't yet accepted that aNum is
meaningful. You've told Coq that [aNum] has
a value of type [nat], but you haven't yet
proven it (or even that it's possible).
*)

(**
What's going on? You noticed the funny
thing that happened over on the right? 
Coq went into "proof mode." It's saying,
"Okay, you've told me that aNum has type
[nat], but now you have to Prove It!"

Coq goes into proof mode, and on the right
gives you a *goal* to prove. You now have
to work with Coq to produce a proof.
*)

Proof.
exact 7.
Qed.

(**
The symbol [aNum] is now defined in the
"environment" of symbol names. Coq has
accepted the definition, and we can now
check the type of [aNum]. What will it be?
*)

Check aNum.
Print aNum.

(** 
Admitted tells Coq to just accept that
the proposition is proved, and to take
the it as an axiom. It's a major cheat,
and it means you haven't really proved
anything at all.
*)

(**
The type declaration [aNum: nat] is what 
we call a type judgment. You can think of
it as a claim, or a proposition, and one
that needs to be proved.
*)

(**
We can and usually (but not always) declare
a type and give a proof at the same time.
*)

Definition aNum2: nat := 4.
Definition aNum8 := 4.

(**
You see, Coq says, "fine, you've given me
a type judgment and proved it, too. Cool!"
*)

(**
Next, let's look at the very first simple
expression that Gregor introduced to his
first year students: (+ 3 4). What do you
expect is the type of this expression?
*)

Check (plus 3 4).

(**
Sure enough, the expression is of type
[nat]. It all seems to be working!
*)

(**
How about evaluating this expression?
In Coq, there's no read-eval-print loop
(REPL), as there is in Racket, so we can't 
just type the expression and get an answer.
What we can use is Coq's command to eval
an expression, [Compute]. It looks like 
this. 
*)

Compute (plus 3 4).

(**
As you can see, Coq reduced the reducible
expressed (redex) to a value and printed
that value, along with its type, over on 
the right.
*)

(**
As you might expect, we can also bind
an expression to an identifier, like this.
*)

Definition aSum: nat := (plus 3 4).
Print aSum.

(** 
Cool. Now an interesting question. Could
we have used the expression [(plus 3 4)]
as a proof of the earlier type judgment?
Let's see.
*)

Definition aNum3: nat.
Proof.
exact (plus 3 4).
Qed.

(**
Indeed!
*)

(**
What is the type of aNum3?
*)

Check aNum3.

(**
What is the value of aNum3.
*)

Print aNum3.

(**
Trick question! The identifier is bound to
an unreduced term. And not only that, but
it's bound to a term that is being used as
a proof.

What happens if we try to [Compute] the 
value of an expression in which aNum3 
appears?
*)

Compute (plus aNum2 aNum3).

(**
Yikes. Coq is saying, well, the answer is
the successor ... of the successor .., of 
the successor ... of the successor of 
aNum3. That is correct, the answer is 4 
more than aNum3, but why won't Coq use
the value that it knows aNum3 has to give
us the final answer? 

Here we get into a concept known as "proof
irrelevance." In a nutshell, [Qed] asks Coq 
to check that a proof is ok (it type checks
it!), and if so, it adds the new, named 
definition to the, environment, and it then
*hides* the proof! Sometimes, though, we'll
need to be able to use the actual value of
a proof later on. In that case, we use the
command [Defined] rather than [Qed], and 
that makes the proof "transparent" rather
than "opaque". Watch.
*)

Definition aNum4 : nat.
Proof.
exact (3 + 4).
Defined.

Check aNum4.
Print aNum4.
Compute aNum4.

(**
Hey, let's do a real proof. What do you
think is the value of this expression?
(plus aNum2 aNum4). Let's write a theorem
and a proof!
*)

Theorem itIs11: (plus aNum2 aNum4) = 11.
Proof.
unfold aNum2.
unfold aNum4.
compute.
reflexivity.
Qed.

Print itIs11.

(**
Now there's a proof who's details we really
don't care about. So we use Qed.
*)


(**
So we've now seen, in Coq, which is to say
in a strongly typed language, four of the
key concepts introduced in Gregor's video.
Let's do some more!

* Expresions
  - literal values
  - constant definitions
  - (reducible) expressions
  - evaluation

In addition, we've seen a whole bunch of
new stuff
    - types and values of types
    - type declaratins as judgments to prove
    - proving such "propositions"
    - writing and providing theorems
*)

(**
Now, go back and look very carefully at the
theorem, and think about the types. What's
going on?
*)

(**
Homework: 

* Watch and study all of Gregor's 1B and 2.

* Download and install Coq and Coq IDE but
  if you're on a Mac, you'll have to use 
  emacs and Proof General, instead.

Run through this whole script.
*)

(**
Have we got some more time? Well then, what
about the rest of Chapter 1a (BSL)?

  - Booleans
  - Conditionals
  - Strings
  - Images
*)

Module mybool.

Inductive mybool: Set := 
  | true: mybool
  | false: mybool.

Definition isTrue: bool -> bool.
Proof.
exact (fun b: bool => b).
Qed.

End mybool.