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 ?

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

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

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`

Inline, not outline — inlining `x`

in `let x := 0 in <body>`

means writing `<body with x replaced by 0>`

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: Jun 18 2024 at 22:01 UTC