## Stream: Coq users

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

#### 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 ?

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

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

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

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

#### 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: Oct 01 2023 at 19:01 UTC