Skip to content

Instantly share code, notes, and snippets.

@atondwal
Created January 20, 2014 23:38
Show Gist options
  • Save atondwal/8531581 to your computer and use it in GitHub Desktop.
Save atondwal/8531581 to your computer and use it in GitHub Desktop.
(**
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment