CODEWITHSUNDEEP
classtype-inferencecoq
jaam
jaam

Reputation: 980

Coq: Resolve an expression to multiple instances

In a scenario like this, I want a single expression to resolve to multiple instances:

Inductive SR: Prop := Sen | Inf.
Parameter CA S: Prop.
Parameter X: SR -> CA -> Prop -> Prop.
Parameter X': SR -> CA -> Prop -> Set.
Parameter XP: SR -> CA -> Prop -> Type.

Definition iX' (t:bool): SR -> CA -> Prop -> Type := if t then X' else XP.

Context `{b:bool}`{c:bool}`{d:bool}`{s:SR}`{t:SR}`{u:SR}`{k:CA}`{l:CA}`{m:CA}`{o:Prop}`{p:Prop}`{q:Prop}.
Parameter foo: iX' b s k o.
Parameter foo'': iX' d u m q.
Parameter ss: S.

Class CON (f:bool) := an: if f then iX' b s k o -> iX' c t l p -> iX' d u m q else S -> S -> S.
Instance coni: CON true := fun (_:iX' b s k o) (_:iX' c t l p) => foo''.
Instance conj: CON false := fun (_:S) (_:S) => ss.

Check (_: CON false) ss.
Check (_: CON true) foo.
Check (_: CON _) ss.
Check (_: CON _) foo. (*Error: The term "foo" has type "iX' b s k o" while it is expected to have type "S".*)

Is there a way to make the instance resolution work w/ both (_: CON _) foo and (_: CON _) ss? If not, try to succeed in a scenario where the class and/or instances are different, while ... in Check ... ss and Check ... foo is identical, and resolves to functions fun (_:S) (_:S) => ss and fun (_:iX' b s k o) (_:iX' c t l p) => foo'', resp.

Upvotes: 1

Views: 97

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

Is there any reason to restrict yourself to instances here? If you're already doing this much hackery, you might as well go a bit further and use tactics in terms in notations.

Ltac mkcon arg :=
  match constr:(Set) with
  | _ => exact ((_ : CON false) arg)
  | _ => exact ((_ : CON true) arg)
  end.

Notation CON_ arg := ltac:(mkcon arg) (only parsing).

Check (_: CON false) ss.
Check (_: CON true) foo.
Check CON_ ss.
Check CON_ foo.

Upvotes: 1

Related Questions