Lecture 03

include some useful libraries

List provides the cons notation "::" "x :: xs" is the same as "cons x xs"

List provides the append notation "++" "xs ++ ys" is the same as "app xs ys"

some interesting types Prop is the type of proofs Just like Set, we use it as a type for things Unlike Set, we mainly use it for the type of facts myTrue is a proposition that holds It has one constructor with no arguments No matter the context, you an always make a value of type myTrue No matter the context, you can always prove myTrue (essentially True)

exact I.

myFalse is the proposition that never holds It has no constructors, and there are no ways to prove myFalse No matter the context, myFalse doesn't hold

inversion does case analysis on a hypothesis for each constructor that could have constructed the hypothesis, we end up with a subgoal for each constructor for False (the builtin equivalent to myFalse), there are 0 constructors

Any type can be a proposition Thus we can prove any type Slightly weird, but it works

exact (list nat). exact nat.

discriminate is a tactic that looks for mismatching constructors under the hood, 1 looks like S (0) and 2 looks like S (S 0) It peels off one S, gets 0 = S 0 0 and S are different constructors, thus they are not equal

Note that even equality is defined, not builtin

What's wrong with this? There's no way to build any objects of type yo

We want to prove that no objects of type yo exist We can prove that any object of that type would mean False Thus there are none

well, that didn't work

but that did!

check out negation It looks just like what we just did

Expression Syntax

Now let's build a programming language! We can define parts of a language as an inductive datatype.

A constant expression, like "3" or "0"

A program variable, like "x" or "foo"

Adding expressions

Multiplying expressions

Comparing expressions

On paper, this would be written as a "BNF grammar" as:

    expr ::= N
          |  V
          |  expr <+> expr
          |  expr <*> expr
          |  expr <?> expr

Coq provides mechanism to define your own notation which we can use to get "concrete syntax" Feel free to ignore most of this, especially the stuff farther right

parsing is classic CS topic, but won't say much more while parsing is still an active research topic in some places, we know how to do it pretty well in a lot of cases we can write functions to analyze expressions Here we're simply going to count the number of const subexpressions in a given expression

same as S O

same as O

same as plus (nconsts e1) (nconsts e2)

Coq also provides existential quantifiers We prove them by providing concrete examples

Here we give a concrete example

Now we have to show that the example we gave satisfies the property

Compute the size of an expression

same as S O

same as plus (esize e1) (esize e2)

and do proofs about programs Show that we always have more nodes than consts

auto will solve many simple goals auto will happily do nothing to your goal as well

omega will solve many arithemetic goals omega will only work if it solves your goal

that proof had a lot of copy-pasta :(

Here we introduce the semicolon ; for any tactics a and b, "a; b" runs a, then runs b on all of the generated subgoals do induction, then on every resulting subgoal do simpl, then on every resulting subgoal do auto, then on every resulting subgoal do omega

note that after the auto, only the Add, Mul, and Cmp subgoals remain, but it's hard to tell since the proof does not "pause"

In order to figure out notation, use Locate

This generates a lot We care about the entry about nats "n <= m" := le n m : nat_scope (default interpretation) Now let's look at the definition

it's a relation defined as an inductive predicate we give rules for when the relation holds anything is less than itself and if something (n) was less than or equal to some other thing (m), then n <= S (m) we can define our own relations to encode properties of expressions Each of the constructors corresponds to how you can prove this fact

Are add and mul commutative? Not as just syntax

specialize gives concrete arguments to hypotheses with forall

inversion is smart

Similarly, we can define a relation for having a variable

we could write boolean functions to check the same properties orb is just or for booleans

the Bool library provides "||" as a notation for orb

That looks way easier! However, as the quarter progresses, we'll see that sometime defining a property as an inductive relation is more convenient We can prove that our relational and functional versions agree This property is that the hasConst function is COMPLETE with respect to the relation Thus, anything that satisfies the relation evaluates to "true" with the function

uh oh, trying to prove something false! it's OK though because we have a bogus hyp!

inversion lets us do case analysis on how a hypothesis of an inductive type may have been built. In this case, there is no way to build a value of type "has_const (Var s)", so we complete the proof of this subgoal for all zero ways of building such a value

here we use inversion to consider how a value of type "has_const (Add e1 e2)" could have been built

built with hc_add_l

subst rewrites all equalities it can

remember notation "||" is same as orb

built with hc_add_r

use fact that orb is commutative

you can find this by turning on auto completion or using a search query

Mul case is similar

Cmp case is similar

now the other direction Here we'll prove that the hasConst function is SOUND with respect to the relation That if hasConst produces true, then there is some proof of the inductive relation

we can prove this case with a constructor

this uses hc_const

Uh oh, no constructor for has_const can possibly produce a value of our goal type! It's OK though because we have a bogus hypothesis.

now do Add case

either e1 or e2 had a Const

consider cases for H

e1 had a Const

e2 had a Const

Mul case is similar

constructor will just use hc_mul_l

constructor will screw up and try hc_mul_l again! constructor is rather dim

OOPS!

Cmp case is similar

we can stitch all these together

• >

<-

all that was only for the true cases! can also use not and do the false cases Here we prove it directly However, we could use has_const_iff_hasConst for a much more direct and simple proof

uh oh, trying to prove something bogus better exploit a bogus hypothesis

proof by contradiction

prove conjunction by proving left and right

Mul case is similar

Cmp case is similar

Since we've proven the iff for the true case We can use it to prove the false case This is the same lemma as above, but using our previous results

do case analysis on hasConst e eqn:? remembers the result in a hypothesis

now we have hasConst e = true in our hypothesis

We have a contradiction in our hypotheses discriminate won't work this time though

For the other case, this is easy

Now the other direction of the false case

crunch down everything in subgoals

get both proofs out of a conjunction by destructing it

case analysis on H0 DISCUSS: how do we know to do this?

auto will chain things for us

Mul case similar

Cmp case similar

Since we've proven the iff for the true case We can use it to prove the false case This is the same lemma as above, but using our previous results

~ X is just X -> False

We can also do all the same sorts of proofs for has_var and hasVar

TODO: try this without copying from above

TODO: try this without copying from above

TODO: try this without copying from above

we can also prove things about expressions

prove left side of disjunction

prove right side of disjunction

case analysis on IHe1

Mul case similar

Cmp case similar

we could have gotten some of the has_const lemmas by being a little clever! (but then we wouldn't have learned as many tactics ;) )

or even better

NOTE: we got another subgoal!