Created
January 20, 2014 23:38
-
-
Save atondwal/8531581 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** | |
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