Stream: Coq users

Topic: tail of vector using recursion


view this post on Zulip walker (Jan 10 2024 at 22:00):

not exactly coq quetion but technique qeustion:

Inductive vec T : nat -> Type :=
| vnil: vec T 0
| vcons (a: T) (n: nat) (v: vec T n): vec T (S n).


Definition vtail T (n: nat) (v: vec T (S n)): vec T n.
:=
    @vec_rect T
    (fun l v =>  match l with | 0 => False | S n' => vec T n end) (*can be easily done without match *)
    _ (* I need a proof of false here *)
    _ (* it is almost match ... and case analysis but I cannot use match or case analysis *)
    (S n) v.

I am not sure what should I be filling in he holes

view this post on Zulip Gaëtan Gilbert (Jan 10 2024 at 22:15):

the second argument of vec_rect should use True not False, and vec T n' not vec T n
then the first hole needs a proof of True (easy)
and the second hole should also be easy

view this post on Zulip walker (Jan 10 2024 at 22:17):

the n and n' is a typo... and it is obvious why, but I cannot see the intuition behind True part

view this post on Zulip walker (Jan 10 2024 at 22:18):

isn't what we are saying that this case is unreachable ?

view this post on Zulip walker (Jan 10 2024 at 22:24):

The function was trivial once I replaced false with true, but I cannot see the intuition:

Definition vtail T (n: nat) (v: vec T (S n)) : vec T n :=
    @vec_rect T
    (fun l v =>  @nat_rect (fun _ => Type) True (fun l' _ => vec T l') l)
    I
    (fun _ n v _ => v) (S n) v.

view this post on Zulip Gaëtan Gilbert (Jan 10 2024 at 22:34):

the case isn't really unreachable, rather we are defining a generalized tail function

 @vec_rect T
    (fun l v =>  @nat_rect (fun _ => Type) True (fun l' _ => vec T l') l)
    I
    (fun _ n v _ => v)

then using it for the specific case of S n
this generalized tail returns the tail for nonzero n, and nothing of interest (True / unit) for 0

view this post on Zulip walker (Jan 11 2024 at 10:24):

I have a follow up question with different example:

Definition vlast T (n: nat) (v: vec T (S n)) : T:=
   @vec_rect T
   (fun l v =>  @nat_rect (fun _ => Type) True (fun _ _ => T) l)
   I
   (fun a' n' v' IH => @vec_rect T (fun l v => T) a' (fun a'' n'' b'' IH' => IH (*problem here*)) n' v')
   (S n) v.

view this post on Zulip walker (Jan 11 2024 at 10:25):

The term IH has type nat_rect (fun=> Type) True (fun=> (fun=> T)) n' while it is expected to have type T.

But then nat_rect (fun=> Type) True (fun=> (fun=> T)) n' is actually T because we are in the second branch of the nested recursor.

view this post on Zulip walker (Jan 11 2024 at 10:26):

I assume this information does not just emerge out of no where, and this information must be passed around somewhere, perhaps in the motive? but I cannot come up with the right technique

view this post on Zulip Pierre Roux (Jan 11 2024 at 10:30):

A bit unrelated but just to be sure you didn't miss it: as you can see, vector is famous for being very painful to use https://github.com/coq/coq/pull/18032 If you don't have a very good reason to use them, it's recommended to go for dependent pairs of lists and proof about their length.

view this post on Zulip walker (Jan 11 2024 at 10:33):

I know it is tricky, that is precisely the point, I am stress testing my own inductive definition implementation, and for that I need indutive type with indices that keep changing. vector felt like good example.

The strategy is to do things in coq first then to make sure it works, then do it in my language.

view this post on Zulip walker (Jan 11 2024 at 10:35):

I thought the good thing about vectors is that they don't need lots of infrastructure unlike other things which will require me to implement equality, and peano, that is restriction because as of now, I am building ast by hand, and don't want to build the whole peano in ast.

view this post on Zulip walker (Jan 11 2024 at 10:35):

but I am open to other alternatives with indices that behave like real indices rather than parameters.

view this post on Zulip Gaëtan Gilbert (Jan 11 2024 at 10:41):

you want to say something like "in the cons a' n' v' case, if v' is nil return a' otherwise recurse (which means use the induction hypothesis IH)"
using the induction hypothesis in the cons _ _ (cons _ _ _) case needs us to update its type from n' to (S something), we use the convoy pattern for this

Definition vlast T (n: nat) (v: vec T (S n)) : T:=
  let P := @nat_rect (fun _ => Type) True (fun _ _ => T) in
   @vec_rect T
   (fun l v =>  P l)
   I
   (fun a' n' v' IH => @vec_rect T (fun n'' _ => P n'' -> T) (fun _ => a') (fun _ _ _ _ IH' => IH') n' v' IH)
   (S n) v.

the convoy pattern is where you do your match/foo_rect with the hypothesis you want to update in the predicate, here fun n'' _ => P n'' -> T
IH' is the update IH
fun _ => a' ignores the updated IH (with type annotation it is fun _ : True => a')

view this post on Zulip Gaëtan Gilbert (Jan 11 2024 at 10:50):

but I am open to other alternatives with indices that behave like real indices rather than parameters.

maybe worth working with equalities a bit

view this post on Zulip walker (Jan 11 2024 at 10:55):

Thanks alot, I didn't know the convoy's pattern trick! And thanks for the equality suggestions!

view this post on Zulip Gaëtan Gilbert (Jan 11 2024 at 11:17):

for fancy index wrangling while stll staying relatively simple there's hedberg's theorem
the following is a specialized proof for the case of singleton types:

Scheme Induction for eq Sort Prop.

Section S.
  Variable A:Type.

  Definition trans_sym_eq {x y:A} (e : x = y) : eq_trans (eq_sym e) e = eq_refl
    := eq_ind_dep A x (fun z e' => eq_trans (eq_sym e') e' = eq_refl)
         eq_refl y e.

  Variable x:A.
  Hypothesis isHProp : forall y:A, x = y.

  Definition left_inv_on y (e:x = y) : eq_trans (eq_sym (isHProp x)) (isHProp y) = e
    := eq_ind_dep A x (fun z e' => eq_trans (eq_sym (isHProp x)) (isHProp z) = e')
         (trans_sym_eq (isHProp x)) y e.

  Definition uip y (e1 e2:x = y) : e1 = e2
    := eq_trans (eq_sym (left_inv_on y e1)) (left_inv_on y e2).
End S.

you can try to understand it and how to generalize it to replace isHProp with eq_dec : forall y, x = y \/ not (x = y)
(the generalized proof is in the stdlib called Eqdep_dec.eq_proofs_unicity_on)

view this post on Zulip Dominique Larchey-Wendling (Jan 18 2024 at 14:01):

One can do this with dependent pattern matching but avoiding eq_rect (ie type cast) like this:

Inductive vec T : nat -> Type :=
| vnil: vec T 0
| vcons (a: T) (n: nat) (v: vec T n): vec T (S n).

Definition is_nz n := match n with 0 => False | S _ => True end.
Definition dpred {n} : is_nz n -> nat :=
  match n with
  | 0   => fun C => match C with end
  | S n => fun _ => n
  end.

Definition vtail T n (v : vec T (S n)) : vec T n :=
  match v in vec _ m return forall h : is_nz m, vec _ (dpred h) with
  | vnil _        => fun C => match C with end
  | vcons _ _ _ v => fun _ => v
  end I.

One could also use the non-dependent pred from the standard library in this case but in general, one needs a default value in excluded cases and using match _ : False with end works in a more generic way.


Last updated: Jun 23 2024 at 04:03 UTC