Why the tactic "apply... with..." cannot be applied to hypotheses?

Using Coq
1

I am wondering why the tactic apply ... with ... cannot be applied to hypotheses.
Here is an example.

Theorem in_not_nil :
  forall A (x : A) (l : list A), In x l -> l <> [].
Proof.
  intros A x l H. unfold not. intro Hl. destruct l eqn:HE.
  - simpl in H. destruct H.
  - discriminate Hl.
Qed.

Lemma in_not_nil_42_take2_no_second_implication :
  forall l : list nat, In 42 l -> l <> [].
Proof.
  intros l H.
  apply in_not_nil with (x := 42).
  apply H.
Qed.

The tactic apply ... with ... works well in this lemma where l <> [] is the goal.

Lemma in_not_nil_42_take2 :
  forall l : list nat, In 42 l -> l <> [] -> true = true.
Proof.
  intros l H1 H2.
  apply in_not_nil in H2 with (x := 42).
  apply H.
Qed.

However, if we turn l <> [] into one hypothesis, it does not work.
I would like to know why it doesn’t work and how we can solve it.
Thank you!

2

Hi,
The reason you cannot apply the theorem on specifically l <> [] when it is in hypotheses is because it is short for l =[] -> False.

You can see it yourself with the following:

Locate “<>”.

Notation
“x <> y” := not (eq x y) : type_scope (default interpretation)

Print not.

not = fun A : Prop => A → False
: Prop → Prop

Once you unfold not in *, you can again use similar forward reasoning that you showed in this example.

3

Thank you for your answers. You mean I need to do unfold not in * before using apply with? It seems that it didn’t work either.

4

Not exactly. Essentially l<>[] is the same as l=[]-> False. Now if you have another hypothesis of the form l=[] (check the example). You can apply chain in the hypothesis to reach a conclusion.

 A: Type
 l: list A
 Negated: l <> []
 H2: l = []
------------------------------
42 = 0

Applying unfold not gets us to this.

 unfold not in *.

 A : Type
 l: list A
 Negated: l = [] -> False
 H2: l = []
------------------------------
42 = 0

apply Negated in H2. 

 A : Type
 l: list A
 Negated: l = [] -> False
 H2: *False*
------------------------------
42 = 0

destruct H2. (*finishes the proof, since anything can be proved from false hypotheses*)

More importantly a<>b is an implication (X->Y) rule and needs this 2 step process of unfolding and application which is where you have the problem.

Refer to Tactics: More Basic Tactics to learn more about this style of reasoning.

5

Yes. I understand your example. However, it seems that this is not exactly the question I asked. I am asking how to use tactic apply ... with .... Could you have a clue about how to solve it? Thank you.

6

Do you mean what does apply ... with ... do? If so then it’s no different than apply tactic. It fixes certain argument values. For example:

 Hyp: forall x y : nat, x + y = y + x
---------------------------
 42 + 5 = 5 + 42

apply Hyp with (x:=42) (y:=5). (*same as `apply (Hyp 42 5)`*)

---------------------------
No more subgoals.

If your question was why can’t you apply ... with ...in H to (H : l <>[]), that’s better explained in the software foundations link from earlier. It’s because l <> [] = (l=[]) -> False where apply doesn’t …apply.

7

Let’s be clear. My question is that apply with works in Lemma in_not_nil_42_take2_no_second_implication and doesn’t work in Lemma in_not_nil_42_take2. I am afraid you didn’t look at my questions clearly.

8

Again, I did read your questions and I am correctly pointing out what you are doing wrong.
You are trying to “backward” reason about the hypothesis which is wrong to do even in paper proofs. Look at the software foundation section relevant here.

In your example of in_not_nil_42_take2. You can apply in_not_nil to H1 not H2.
Applying to H1 is essentially reasoning “forward”.

 l: list nat
 H1: In 42 l
 H2: l <> []
----------------

apply in_not_nil in H1.

 l: list nat
 H1: l <> []
 H2: l <> []
----------------

In verbose: It is established that (42 is in l : H1), now from previous result (in_not_nil) you can conclude that l is not empty.

However what you are attempting is apply to H2: "I know l is not empty, from that I want to establish that 42 is in l, which is wrong. There might be many reasons why l is not empty say perhaps 5 is in l.
In fact to say that “some x” is in l you need to prove a result similar to in_not_nil in the other direction (which is l <> [] -> exists x, In x l).

 correct: forall l : list nat, l <> [] -> exists x : nat, In x l
 l: list nat
 H1: In 42 l
 H2: l <> []
------------------------------

apply correct in H2.

 correct: forall l : list nat, l <> [] -> exists x : nat, In x l
 l: list nat
 H1: In 42 l
 H2: exists x : nat, In x l (*Saying some x is in l and hence it is not empty*)
------------------------------

I hope this clarifies your questions. I don’t think I can add anything new outside of this.
Regards.

9

I am really sorry. I misunderstood you. The lemma like correct works very well. So, “backward reason” can never work on hypotheses (including applying external lemmas) in Coq. Thank you very much for your help!

1 Like