Another Proof From Logical Foundations Exercises

Using Coq
1

I’m working through the list exercises of the Lists portion of Logical Foundations (still) and I’ve got to one that I can’t quite finish proving.

Here’s the code:

Theorem eqblist_refl: forall l:natlist,
   true = eqblist l l.
Proof.
   intros l. induction l as [| n l' IHl'].
   - simpl. reflexivity.
   - simpl. rewrite <- IHl'.
Qed.

The first half of the induction is proven; it’s the second half that I can’t quite seem to figure out. And this is what I get in the output:

1 subgoal
n : nat
l' : natlist
IHl' : true = eqblist l' l'
______________________________________(1/1)
true = (n =? n) && true

For the life of me I can’t figure out how to prove n =? n is true. I mean it seems as if it should be provable by simple reflexivity but that doesn’t seem to do it. Can anyone please give me a small nudge in the correct direction?

2

What’s the reason you are proving true = eqblist l l by induction on l and not just by reflexivity? :slight_smile: (Answering that question hopefully brings you a little closer to an answer to your question.)

3

eqblist l l should be defined as a fixpoint on lists; that’s why eq_refl won’t work here.

Have a look at the definition of =?:

About "=?".
>> Basics.eqb : nat -> nat -> bool

Print Basics.eqb.

Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => eqb n' m'
            end
  end.

You should be able to prove that n =? n = true as a lemma by induction on n. Indeed, a quick search reveals that there is already a lemma for this:

Search "=?".

>> eqb_refl: forall n : nat, true = (n =? n)
>> ...
1 Like
4

It is defined as a fixpoint. It’s just defined further up in the code. Here’s the definition for reference:

Fixpoint eqblist (l1 l2: natlist) : bool :=
   match l1,l2 with
   | nil, nil => true
   | nil, _ => false
   | _, nil => false
   | h1::t1, h2::t2 => (andb (h1 =? h2) (eqblist t1 t2))
   end.

Beyond that, I’m trying to work through an exercise so I’m not sure that I’ve pulled in the definitions from the standard libraries (or whatever they’re called in Coq). I mean when I do About "=?". I get this:

eqb : nat -> nat -> bool

eqb is not universe polymorphic
Arguments eqb (_ _)%nat_scope
eqb is transparent
Expands to: Constant LF.Basics.eqb

I’m guessing the Basics.eqb you’re referencing is a built in eqb.

5

Hmm. I’ve tried proving it by reflexivity but that doesn’t get me anywhere. But I’ll give it some thought. Maybe the light of epiphany will break through at some point :slight_smile: Thanks!

6

No, @yforster meant: Why can’t you prove eqblist_refl by reflexivity? For the same reason, you can’t prove n =? n = true by reflexivity.

7

The eqb in the file is in fact not an ‘inbuilt’ function, as Coq doesn’t has any ‘inbuilt’ functions. Even eq is defined inside Coq! (Try Print eq.)

However, in fact there is a function with the same name in Coq’s standard library, but which is not imported by default:

From Coq Require Import Nat.
About eqb.
>> eqb : nat -> nat -> bool
>>
>> eqb is not universe polymorphic
>> Arguments eqb (_ _)%nat_scope
>> eqb is transparent
>> Expands to: Constant Coq.Init.Nat.eqb

In Coq, there can be multiple definitions with the same name, which must, however, be defined in different modules. To avoid confusion, every definition has a fully quantified name, which is in the last line of the About command.

8

I said built in but I meant a standard function; I was simply using the wrong terminology.

I know that Coq doesn’t have predefined functions but I also know there’s a standard library to handle common tasks. That’s what I was trying to say–that you were referencing a standard library function and I was using something that I had defined via the prior exercises in the text.

The part about it being ok to have mutliple definitions with the same name–well that’s new to me so thanks!

And thank you for taking the time to assist!