## Stream: Equations devs & users

### Topic: Why are `where` clause obligations reversed?

#### Jason Gross (Nov 15 2022 at 19:50):

If I write

``````    | red_view_Case ci p c brs π with RedFlags.iota flags := {
| true with inspect (reduce c (Case_discr ci p brs :: π) _) := {
| @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
| @exist (args, ρ) prf' with cc_viewc t := {
| ccview_construct ind' c' inst' with inspect (nth_error brs c') := {
| exist (Some br) eqbr := rec reduce (iota_red ci.(ci_npar) p args br) π ;
| exist None bot := False_rect _ _ } ;
| ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
| @exist (Some (narg, fn)) eq' :=
rec reduce (tCase ci p (mkApps fn args) brs) π ;
| @exist None bot := False_rect _ _
} ;
| ccview_other t ht := give (tCase ci p (mkApps t args) brs) π
}
}
} ;
| false := give (tCase ci p c brs) π
} ;
``````

I get a bunch of obligations.

If move the inner match to a where clause, as in

``````    | red_view_Case ci p c brs π with RedFlags.iota flags := {
| true :=
red_view_Case_helper (inspect (reduce c (Case_discr ci p brs :: π) _))
where
red_view_Case_helper : { v | v = reduce c (Case_discr ci p brs :: π) _ }
-> { t' : term * stack | forall Σ (wfΣ : abstract_env_ext_rel X Σ), Req Σ Γ t' (_,π) /\ Pr t' π /\ Pr' t' } := {
| @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
| @exist (args, ρ) prf' with cc_viewc t := {
| ccview_construct ind' c' inst' with inspect (nth_error brs c') := {
| exist (Some br) eqbr := rec reduce (iota_red ci.(ci_npar) p args br) π ;
| exist None bot := False_rect _ _ } ;
| ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
| @exist (Some (narg, fn)) eq' :=
rec reduce (tCase ci p (mkApps fn args) brs) π ;
| @exist None bot := False_rect _ _
} ;
| ccview_other t ht := give (tCase ci p (mkApps t args) brs) π
}
}
} ;
| false := give (tCase ci p c brs) π
} ;
``````

the obligations arising from the `where` function show up in reverse order. Why is this?

Last updated: Jan 29 2023 at 16:02 UTC