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

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!

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.

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.

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.

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.

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.

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.

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.

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