walker (Apr 17 2022 at 11:59): 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 13 2024 at 01:02 UTC