theorem or_eqv_ff1

Stream: general

[Phiroc]

Hello,
I am having trouble implementing the following theorems in *Verified Functional
Programming in Agda*:

-- p. 28
theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 ∨ b2 = ff → b1 = ff
| ff p := rfl
| tt := absurd

-- p. 31
theorem or_eqv_ff1' :
    ∀{b1 b2}, b1 ∨ b2 = ff → b1 = ff
| ff p := rfl
| tt p := p

I think the implications are causing a problem, but am not sure.
Could someone please help?

Thanks.

Phiroc

[Reid Barton]

I think there are some syntactic issues and maybe also some deeper semantic issues.

[Reid Barton]

What do the proofs look like in Agda?

[Reid Barton]

For starters, each of your functions has three arguments (b1, b2 and the proof that b1 ∨ b2 = ff) but you only match two things.

[Reid Barton]

Then, ∨ means "or" of Props, not bools. Actually I don't know how Lean is intepreting your theorem statement.

[Phiroc]

||≡ff1 : ∀ {b1 b2} → b1 || b2 ≡ ff → b1 ≡ ff
||≡ff1 {ff} p = refl
||≡ff1 {tt} ()

||≡ff1 : ∀ {b1 b2} → b1 || b2 ≡ ff → b1 ≡ ff
||≡ff1 {ff} p = refl
||≡ff1 {tt} p = p

[Johan Commelin]

Logical operations are prefixed with b, so it's bnot, bor, band...

[Reid Barton]

So I think in Agda you don't write implicit arguments (like b2) on the left side of an equation unless you choose to, in Lean you do.

[Johan Commelin]

It's too bad they aren't in the bool namespace... because then you could've written p.or q

[Reid Barton]

In Agda {ff} is matching b1 and there is nothing for b2

[Phiroc]

I think p matches b2

[Reid Barton]

It doesn't, else how could the very last line ... p = p type check?

[Phiroc]

The book says:

This is the same as the earlier proof, but for the second clause of the definition, wehave
an actual defining equation that just returns the proof p of the impossible assumption.
The type of p is definitionally equal to tt ≡ ff, which is what we have for the desired
result with b1 instantiated to tt.

[Phiroc]

Regarding the first version of the theorem, the book says:

After this, we have a variable p corresponding to the sole explicit argument of this
proof, namely, the proof of our assumption. We actually do not need to use this
variable on the right-hand side in this case, because if we are in the case where b1
is ff, then our desired result is definitionally equal to just ff ≡ ff. So this equation
has just refl on the right-hand side, to prove that trivial equation ff ≡ ff.

[Reid Barton]

Right, p is the proof. Not b2.

[Phiroc]

Can you do pattern matching which includes proofs, in Lean, e.g. ff p above?

[Kevin Buzzard]

sure

[Reid Barton]

The first problem that we're discussing is that in Lean you have to match b2 explicitly and you haven't done it.

[Phiroc]

Here's Lean's rant about the first theorem:

bool-thms.lean:55:7: error
invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
↥ff
bool-thms.lean:55:7: error
equation type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
↥ff ∨ p = ff → ↥ff = ↥ff

[Phiroc]

This doesn't work either:

theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 ∨ b2 = ff → b1 = ff
| ff tt := rfl

[Reid Barton]

Okay so in fact Lean had a totally different interpretation of your statement.
The equivalent of Agda's || is Lean's bor as Johan wrote earlier. Not ∨.

[Kevin Buzzard]

rfl proofs X = X and you want to prove X -> X

[Kevin Buzzard]

But you are not using the correct "or" operator for bool so nothing will work

[Phiroc]

I'll try bor.

[Kevin Buzzard]

you're using the or which works on Propositions, not on booleans.

[Bryan Gin-ge Chen]

You should be able to use || for bor since it's declared as notation in the core library.

[Reid Barton]

Phiroc said:

This doesn't work either:

theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 ∨ b2 = ff → b1 = ff
| ff tt := rfl

Now you are matching b2, but you still have to match the third argument too :slight_smile:

[Reid Barton]

I'm not sure how many of verified functional programming, Agda, and Lean are new to you, but if it's more than one, what you are trying to do sounds very difficult.

[Reid Barton]

I mean reading the book and translating it into Lean generally, not proving or_eqv_ff1 in particular.

[Phiroc]

I managed to make the first pattern-match work!

theorem or_eqv_ff1 :
    ∀{b1 b2}, bor b1 b2 = ff → b1 = ff
| ff tt p := rfl

[Reid Barton]

By "match", I didn't necessarily mean you have to split into two cases for tt and ff--you can put a variable b2 there, or _.

[Mario Carneiro]

theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 || b2 = ff → b1 = ff
| ff _ _ := rfl

[Mario Carneiro]

I think you don't have to match on the second argument because in lean it's defined by cases only on the first argument

[Phiroc]

Why do you need p (the third parameter)?

[Kevin Buzzard]

because you're making a function with three inputs

[Reid Barton]

Try #check or_eqv_ff1 now that you proved it (or at least came close enough)

[Mario Carneiro]

You could write this:

theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 || b2 = ff → b1 = ff
| ff _ := λ _, rfl

but now lean complains that the match is nonexhaustive. What's happening is that lean is actually matching on the third argument (the proof) in all the impossible cases to prove they are impossible, and if you take it out of the match then lean requires branches for both ff and tt

[Phiroc]

theorem or_eqv_ff1 :
    ∀{b1 b2}, bor b1 b2 = ff → b1 = ff
| ff _ _ := rfl
| absurd

[Phiroc]

... but it doesn't check :-(

[Kevin Buzzard]

Did you read the error?

[Mario Carneiro]

You can explicitly prove the absurd cases like this:

theorem or_eqv_ff1 :
    ∀{b1 b2}, b1 || b2 = ff → b1 = ff
| ff _ := λ _, rfl
| tt _ := λ h, false.elim (bool.ff_ne_tt h.symm)

[Mario Carneiro]

| absurd is not valid syntax

[Kevin Buzzard]

absurd here means "let b1 be absurd"

[Kevin Buzzard]

I think you have bitten off more than you can chew. Do you know about pattern matching in general?

[Reid Barton]

If you want to write Lean then I think it will be much easier to start with a book that teaches Lean.

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

[Phiroc]

I've done a bit of Idris programming.

[Kevin Buzzard]

Why don't you read a Lean book? Then all the proofs in the book will work

[Reid Barton]

If you want to read these languages then you can get by with knowledge from a similar language but writing is a different matter.

[Kevin Buzzard]

https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf

[Mario Carneiro]

that link isn't working for me btw, did Jasmin break it with a recent update?

[Kevin Buzzard]

wgetting it works fine for me

[Johan Commelin]

@Mario Carneiro you are probably using a fancy browser... You should browse the web RMS style :stuck_out_tongue_wink:

[Phiroc]

I'll go throught the books. Many thanks.

[Kevin Buzzard]

Ask if you don't follow something in the books. Theorem Proving In Lean is an excellent place to start for someone with a computer science background.