## Stream: Coq users

### Topic: snoc induction

#### Adrián García (Jul 25 2021 at 22:35):

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)".
``````

#### Adrián García (Jul 25 2021 at 22:37):

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
``````

#### Théo Winterhalter (Jul 25 2021 at 22:43):

`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`.

#### Adrián García (Jul 25 2021 at 22:48):

Wow, thank you! Completely right

#### Paolo Giarrusso (Jul 26 2021 at 01:04):

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

#### Adrián García (Jul 26 2021 at 01:40):

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!

#### Adrián García (Jul 26 2021 at 02:01):

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'`

#### Paolo Giarrusso (Jul 26 2021 at 08:32):

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?

#### Adrián García (Jul 27 2021 at 05:22):

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 :/

#### Paolo Giarrusso (Jul 28 2021 at 04:07):

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.

#### Paolo Giarrusso (Jul 28 2021 at 04:08):

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

#### Paolo Giarrusso (Jul 28 2021 at 04:09):

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

#### Paolo Giarrusso (Jul 28 2021 at 04:11):

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

#### Paolo Giarrusso (Jul 28 2021 at 04:17):

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).

#### Paolo Giarrusso (Jul 28 2021 at 04:20):

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

Last updated: Oct 05 2023 at 02:01 UTC