Follow-ups to the compositional chain-lemma layer (partial_of/captures_of/write_of, chain lemmas over fun_post_of; see #20273 for the base design):
-
Type-generic lemmas via per-instantiation verification. partial_of/captures_of are closed-world definitions over the session's closure variants, so in a generic context they would be evaluated at skolemized types where no variants exist — premises become vacuously false while instantiations discharge them, which is unsound to transfer. They are currently rejected in generic functions/lemmas. The fix is the prover's standard instance-check pattern: verify a generic lemma at each type instantiation occurring at apply sites (mono principle), then lift the rejection. This enables the fully generic, stdlib-shippable for_each_chain<A, T> (today it is written per element/accumulator type, generic in the step function).
-
Multiple / mixed captures. v1 scope is a single &mut capture at prefix position (mask 0b1). Generalize captures_of (tuple-valued or indexed) and the recognizer to arbitrary masks.
-
forall .. apply trigger ergonomics. Quantified lemma instantiation without explicit triggers can send the caller VC into a matching explosion (40s timeout on the chain tests); explicit triggers ({apply_all(f, v, k)}) are load-bearing. Consider deriving default triggers from the lemma's conditions instead of Boogie's inference.
Filed by Claude (AI agent) on behalf of @wrwg.
Follow-ups to the compositional chain-lemma layer (
partial_of/captures_of/write_of, chain lemmas overfun_post_of; see #20273 for the base design):Type-generic lemmas via per-instantiation verification.
partial_of/captures_ofare closed-world definitions over the session's closure variants, so in a generic context they would be evaluated at skolemized types where no variants exist — premises become vacuously false while instantiations discharge them, which is unsound to transfer. They are currently rejected in generic functions/lemmas. The fix is the prover's standard instance-check pattern: verify a generic lemma at each type instantiation occurring atapplysites (mono principle), then lift the rejection. This enables the fully generic, stdlib-shippablefor_each_chain<A, T>(today it is written per element/accumulator type, generic in the step function).Multiple / mixed captures. v1 scope is a single
&mutcapture at prefix position (mask0b1). Generalizecaptures_of(tuple-valued or indexed) and the recognizer to arbitrary masks.forall .. applytrigger ergonomics. Quantified lemma instantiation without explicit triggers can send the caller VC into a matching explosion (40s timeout on the chain tests); explicit triggers ({apply_all(f, v, k)}) are load-bearing. Consider deriving default triggers from the lemma's conditions instead of Boogie's inference.Filed by Claude (AI agent) on behalf of @wrwg.