Stream: Coq users

Topic: `Set Program Cases.` does not work as expected.


view this post on Zulip walker (Apr 17 2022 at 11:59):

Lets consider this snippet (please ignore all the fancy syntax it is not relevant).

Program Definition blocks (s: vec nat 81) (i: nat | i < 9) : vec nat 3 :=
let x := 0 in
  s [[ x .... (x + 3) ]].
Next Obligation.

About right here I have to prove that

vec nat 81  {i : nat | i < 9}  let x := 0 in  en : nat, en < 81) (x + 3)

The most important part is let x := 0 in part

But If I change the blocks function to be something like:

Program Definition blocks (s: vec nat 81) (i: nat | i < 9) : vec nat 3 :=
let (x, y) := (0, 0) in
s [[ x .... (x + 3) ]].
Next Obligation.

The theory becomes stronger and I cannot prove it because information about x is lost:

vec nat 81  {i : nat | i < 9}   x : nat, nat   en : nat, en < 81) (x + 3)

I checked Program documentation and it should have worked but the destruct statement here for some reason does not work. any ideas what is going on ?

view this post on Zulip Paolo Giarrusso (Apr 17 2022 at 14:19):

Probably just a bug in the transformation; replacing the let by a pattern match should fix that.

view this post on Zulip Paolo Giarrusso (Apr 17 2022 at 14:20):

(and of course in this case you could inline the bindings of x and y, but I assume you can't in the real example)

view this post on Zulip walker (Apr 17 2022 at 14:33):

What do you mean by outline the bindings of x and y ?
I will open an issue for it though.

I was able to fix it by using match... with instead of let ... in

view this post on Zulip Paolo Giarrusso (Apr 17 2022 at 17:39):

Inline, not outline — inlining x in let x := 0 in <body> means writing <body with x replaced by 0>

view this post on Zulip Paolo Giarrusso (Apr 17 2022 at 17:39):

in your specific example, instead of let (x, y) := (0, 0) you could use let x := 0 in let y := 0 in <body> (this isn’t inlining), or just <body with x and y replaced by 0> (this is inlining)


Last updated: Feb 01 2023 at 12:30 UTC