COQ :이 같은 시나리오에서 여러 인스턴스

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.