CODEWITHSUNDEEP
coq
Sebastian Fisher
Sebastian Fisher

Reputation: 75

Is there a more elegant way to convince coq that a list based hypothesis is a contradiction?

I was working through a simple lemma and came across a situation where neither the contradiction or injection tactics were as powerful as I might have expected.

Theorem list_app_single: forall (T : Type) (x : T) (l1 l2 : list T),
   l1++[x] =  l2++[x] -> l1 = l2.
Proof.
intros. generalize dependent l2. induction l1.
  - intros. induction l2.
  --  reflexivity.
  -- inversion H.

Stopping here the proof state is:

1 subgoal
T : Type
x, x0 : T
l2 : list T
H : [ ] ++ [x] = (x0 :: l2) ++ [x]
IHl2 : [ ] ++ [x] = l2 ++ [x] -> [ ] = l2
H1 : x = x0
H2 : [ ] = l2 ++ [x0]
______________________________________(1/1)
[ ] = x0 :: l2

Clearly H2 is not true, but coq doesn't see this when applying the discriminate tactic. Is there a tactic that is more appropriate that can resolve that H2 is in fact false?

Edit: Made the question more focused on a specific tactic to overcome limitations of discriminate.

Upvotes: 0

Views: 148

Answers (3)

larsr
larsr

Reputation: 5811

I'm partial to @Theo's solution. It is easy to start destructing terms to the left and to the right, but by doing that one starts to reason on a too low level - reasoning about the implementation of the data rather than about the properties, which makes it less likely for the proof to carry over to other situations.

So if you want just "one tactic that works" then destruct is often useful. You can solve you goal with

  now destruct l2.

But if you want your proof to reason in the theory of the things you reason about - lists - then this proof does just that.

  enough (@length T [] <> 0) by auto.
  rewrite H2, app_length, PeanoNat.Nat.add_comm; auto.

Upvotes: 1

Th&#233;o Winterhalter
Th&#233;o Winterhalter

Reputation: 5108

To complete @Andrey's answer, discriminate indeed applies on equalities featuring different constructors like [] = x :: l. A solution to this problem can be achieved by adding another observation on top of your equality. Here for instance, you can observe that the lengths of such expressions wouldn't match: From [] = l ++ [x] you obtain length [] = length (l ++ [x]) which simplifies to 0 = length l + 1.

From Coq Require Import List Lia.
Import ListNotations.

Lemma foo :
  forall (A : Type) (l : list A) (x : A),
    [] = l ++ [x] ->
    False.
Proof.
  intros A l x e.
  apply (f_equal (@length A)) in e.
  rewrite app_length in e. simpl in e. lia.
Qed.

Notice that in the end, I apply the lia tactic to derive a contradiction from 0 = n + 1.

This method can be very useful in cases where just destructing l wouldn't work right away. If you have discriminations that you perform often, then it might be worth it to have your own discr tactic to do it for you.

Upvotes: 3

Andrey
Andrey

Reputation: 750

To use the discriminate tactic, you need the "top" terms of parts your expression to be constructors (after simplifying). So, the discriminate can see [after some 'thinking'] that the constructors are different.

You do not have constructor on the top of the right part of equality in H2. Namely, l2 ++ [x0] is not a constructor. It is an application of function app (another name of ++ operator) which has two parameters, namely l2 and [x0]. So, your expression looks like

H2 : [ ] = app l2 [x0]

And the right part is obviously not a constructor.

What you can try is to destruct l2.. Since the app function works by matching its first argument then after the simplifying (in H2), top right part of H2 will be a constructor. And the discriminate will be able to finish the proof.

As for another, more smart tactic which able to do it: as far as I can see a general solution is impossible here (we should fall into the halting problem). But I think that after some research somebody could create something more smart then just discrimite. You can see an example of such tactic with good explanation of how it works (the tactic is named crush) in Certified Programming with Dependent Types book by Adam Chlipala.

Namely crush might not be able to solve this particular problem. But I think you could write example of such tactic using techniques the author suggests.

Upvotes: 2

Related Questions