Repository navigation
Case split tactic by "real" pattern matching #27
Description
Given the following (contrived but based on a real world) definition:
f : Bool → Bool → Bool
f true false = true
f x y = trueId like to write a tactic that solves:
p : ∀ (x y : Bool) → f x y ≡ trueIterated case (from Tactic.Case) doesn't cut it:
p x y = by (case x (case y (quoteTC refl >>= λ t → unifyWithGoal t)))I suspect it is because case doesn't do real pattern-matching but instead introduces pattern lambdas. This is not enough for Agda to compute.
Activity
WhatisRT commentedon Mar 27, 2025
IIRC
caseworks by basically generating code of the shapecase x of λ where .... Note that this is the non-dependingcase_of_, so it can't specialize the type in the branches of the lambda. So to fix this, it should instead generatecase x returning M of λ where ..., where we need to generate the motiveMourselves by abstracting and generalizingxfrom the goal type.Note that
casewouldn't be able to do the regular LHS pattern matching, because it's in a term position. And(λ where ...) xis also not viable, because this always fails to infer the motive. So I don't think there's a shortcut here.