I'm trying to prove a lemma for snoc slists, and I'm trying to change the term `S n - n`

with `S 0`

using `change_no_check`

, but after `Qed`

, I get the following error:

```
Illegal applicatiocoq
The term "eq_ind_r" of type
"forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, y = x -> P y"
cannot be applied to the terms
"nat" : "Set"
"S n0" : "nat"
"fun n : nat =>
match n - n0 with
| 0 => None
| S _ => match n - n0 - 1 with
| 0 => Some A
| S n' => slist_nth_aux G n'
end
end = Some A" : "nat -> Prop"
"eq_refl" : "Some A = Some A"
"slist_length G" : "nat"
"H" : "slist_length G = S n0"
The 4th term has type "Some A = Some A" which should be coercible to
"(fun n : nat =>
match n - n0 with
| 0 => None
| S _ => match n - n0 - 1 with
| 0 => Some A
| S n' => slist_nth_aux G n'
end
end = Some A) (S n0)".
```

This is the proof and the current goal in the "change_no_check" line:

```
Lemma nth_snoc:
forall {X: Type} (n : nat) (G : slist X) (A : X),
slist_length G = n -> (G, A)!n = Some A.
Proof.
intro X.
induction n.
- intros.
apply length_empty in H.
rewrite H.
reflexivity.
- intros.
unfold slist_nth.
simpl.
rewrite H.
change_no_check (S n - n) with (S 0).
reflexivity.
Qed.
```

```
1 subgoal
X : Type
n : nat
IHn : forall (G : slist X) (A : X), slist_length G = n -> (G, A) ! n = Some A
G : slist X
A : X
H : slist_length G = S n
______________________________________(1/1)
match S n - n with
| 0 => None
| S _ => match S n - n - 1 with
| 0 => Some A
| S n' => slist_nth_aux G n'
end
end = Some A
```

`S n - n`

is not convertible to `S 0`

, maybe you should use `replace (S n - n) with (S 0)`

instead. The proof can then be discharged by `lia`

.

Wow, thank you! Completely right

And you usually want change over change_no_check; the former will give you an error right away.

Yes, it's just that I was not able to find a way to complete the proof and I felt in desperation a little bit. Thanks!

Also, I'm trying to prove this:

```
Lemma nth_concat:
forall {X: Type} (G' G: slist X) (k: nat),
k < (slist_length G) -> (G;G')!k = G!k.
```

that means, with `k`

smaller than the length of a snoc list `G`

, `(G;G')!k = G!k`

means that looking for the `k`

-th element in the concatenation `(G; G')`

means looking for it in just `G`

, would you recommend doing it by induction on `k`

or structural induction on `G'`

? I'm not able to prove it by induction on `G'`

How are ! and ; defined? I'm wondering whether structural Induction on G would make sense... Either way, have you generalized the variables you're not inducting on?

Well, my snoc lists are defined as:

```
Inductive slist (X: Type): Type :=
| empty : slist X
| snoc : slist X -> X -> slist X.
```

then ! and ; defined as:

```
Fixpoint slist_nth_aux {X : Type} (l : slist X) (n : nat)
: option X :=
match l with
| empty => None
| G', x => match n with
| 0 => Some x
| S n' => slist_nth_aux G' n'
end
end.
Global Hint Unfold slist_nth_aux : slist.
Definition slist_nth {X : Type} (l : slist X) (n : nat) : option X :=
match slist_length l - n with
| 0 => None
| other => slist_nth_aux l (slist_length l - n - 1)
end.
Notation " G ! n " := (slist_nth G n) (at level 20).
```

```
Fixpoint conc {X: Type} (G G': slist X) : slist X :=
match G' with
| empty => G
| snoc D q => snoc (conc G D) q
end.
Global Hint Unfold conc : slist.
Notation " G ; D " := (conc G D) (at level 20).
```

and yes, I'm using `intros X G'`

to avoid introducing any other variable, but I'm not able to find a way to complete the proof :/

Thanks! Recursion on G' looks good, but it's probably easier to use recursion to prove a lemma on slist_nth_aux, not slist_nth: have the proof structure mirror the definition structure, in the simplest case.

Because you need in the recursive case is a lemma about slist_nth_aux, not slist_nth.

(in this case, maybe you can get away without this trick, but not in general)

Then induction on G' and case analysis on k should help.

To find the right statement, I'd start the proof about slist_nth, unfold it, and do case analysis on the scrutinee (neither can be 0).

I haven't checked the above strategy in Coq, but I have some more concrete idea of how it'd go.

Last updated: Jun 14 2024 at 20:01 UTC