Stream: Coq users

Topic: snoc induction


view this post on Zulip 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)".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adrián García (Jul 25 2021 at 22:48):

Wow, thank you! Completely right

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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'

view this post on Zulip 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?

view this post on Zulip 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 :/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 28 2021 at 04:09):

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

view this post on Zulip Paolo Giarrusso (Jul 28 2021 at 04:11):

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

view this post on Zulip 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).

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC