CODEWITHSUNDEEP
coq
gust
gust

Reputation: 945

Make two arbitrary variables the same in Coq

I have the following coq code:

Theorem filter_exercise : forall (X : Type) (l lf : list X) (test : X -> bool)
                             (x : X),
     filter test l = x :: lf ->
     test x = true.
Proof.
  intros X l lf test x eq.
  induction l as [|l' l].
  - inversion eq.
  - inversion eq as [H].

Which gives me:

  X : Type
  l' : X
  l, lf : list X
  test : X -> bool
  x : X
  eq : filter test (l' :: l) = x :: lf
  testEq : test x = false
  IHl : filter test l = x :: lf -> false = true
  ============================
  filter test l = (if test l' then l' :: filter test l else filter test l)

Here, if I could just say that because test x = false and both x and l' are universally quantified variables of type X, then I'd be done with the proof.

However, that's a semantic argument, and I'm not sure how to do that in Coq. Am I going down the wrong path?

EDIT

For posterity, this is the solution I ultimately obtained:

Theorem filter_exercise : forall (X : Type) (l lf : list X) (test : X -> bool)
                             (x : X),
     filter test l = x :: lf ->
     test x = true.
Proof.
  intros X l lf test x eq.
  induction l as [|l' l].
  - inversion eq.
  - simpl in eq. destruct (test l') eqn:testl'.
    + inversion eq. rewrite <- H0. apply testl'.
    + apply IHl. apply eq.
Qed.

Upvotes: 1

Views: 156

Answers (2)

Lucien David
Lucien David

Reputation: 320

Your argument that test x = false -> test l' = false is not true, as both variables x and l are universally quantified, and thus can have any value. You could just have a specific relationship between both variables in your hypothesis, but here it is not the case, except the relationship filter test (l' :: l) = x :: lf, that tells you that x could be an element of l which has not been filtered by test (but it also might be l').

You should not use inversion here, as your problem is really simple. You idea to perform an induction is fine however :

  • Try first to simplify several hypothesis.
  • Then see if there are different cases to deal with, and use destruct when needed (on the value of test l' in this problem)
  • You should be able to solve the problem then (the most complicated tactic you might have to use is injection)

Upvotes: 1

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

I am not sure what you mean by "semantic argument", but this proof strategy is not correct, neither on paper nor in Coq. Consider, for instance, the following statement:

Lemma faulty : forall n m : nat, even n -> even m.
Proof. Admitted.

By your logic, if n is even, then m should also be even, since both are universally quantified variables of type nat. However, precisely because they are universally quantified, they can instantiated to different values of nat, thus yielding obviously contradictory statements. For instance, if we instantiate faulty with 2 and 1, we should be able to conclude that 1 is even, which is not true.

Upvotes: 2

Related Questions