コックは、このようなシナリオでは、複数のインスタンス

Question

に式を解決し、私は単一の式が複数のインスタンスに解決したい：

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".*) 

は、インスタンスの解像度の仕事を作るための方法があります/ wの両方 (_: CON _) fooと (_: CON _) ss？そうでない場合は、クラスやインスタンスが異なるシナリオで成功してください。 ...の Check ... ssと Check ... fooは同じで、関数 fun (_:S) (_:S) => ssと fun (_:iX' b s k o) (_:iX' c t l p) => foo''、respに解決されます。

Answer 1

ここにインスタンスを限定する理由はありますか？あなたがすでにこのようなハッカーをしているのであれば、もう少し進んで、表記の面で戦術を使うかもしれません。

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.