The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

The following looks for me as a fault in Coq8.0  (I am using Windows).

Error message is issued with the command 'Qed', when the proof of the lemma B_Cases_inv is completed:

Error: Illegal application (Type Error):
The term "B_Sym" of type "forall x y : bool, BEqual x y -> BEqual y x"
cannot be applied to the terms
 "B_Cases0 x2 a b" : "CProp"
 "a" : "CProp"
 "B_TrueCase (R:=BEqual) (a:=a) b H1 (B_Refl a)"
   : "BEqual (B_Cases BEqual x2 a b) a"
The 3th term has type "BEqual (B_Cases BEqual x2 a b) a"
which should be coercible to "BEqual (B_Cases0 x2 a b) a"

Regards,

Jevgenijs.

 

PS.  Here is the script.

 

Set Implicit Arguments.
Unset Strict Implicit.

 

Parameter bool : Type.
Parameter PROP:bool->Prop.
Coercion PROP:bool >->Sortclass.
Parameter BEqual : bool -> bool -> bool.
Axiom B_Refl : forall x : bool, BEqual x x.
Axiom B_Sym : forall x y : bool, BEqual x y -> BEqual y x.
Axiom B_Trans : forall x y z : bool, BEqual x y ->BEqual y z -> BEqual x z.
Parameter true : bool.
Parameter false : bool.
Axiom Tautology: true.
Axiom Contradiction : forall x : bool, false -> x.
Axiom B_Replace : forall x y : bool, BEqual x y  ->x ->y.
Axiom  B_Decide :  forall x y : bool, (BEqual x true -> y) -> (BEqual x false -> y) ->y.
Parameter B_Cases: forall  (R : bool -> bool -> bool), bool -> bool -> bool -> bool.
Axiom B_TrueCase :
    forall  (R : bool -> bool -> bool) (a b : bool) (x : bool),
    BEqual x true -> R a a ->R (B_Cases R x a b) a.
Axiom
  B_FalseCase :
    forall  (R : bool -> bool -> bool) (a b : bool) (x : bool),
    BEqual x false -> R b b -> R (B_Cases R x a b) b.

 

Structure CSetoid : Type := Build_CSetoid
   {cs_crr     :> Type;
   cs_eq : cs_crr -> cs_crr -> bool}.

 

Definition CProp := Build_CSetoid (cs_crr:=bool) BEqual.
Definition Equal:=(fun (X:CSetoid)(x y:X)=>(cs_eq x y):CProp).
Definition B_Cases0:= (fun (x a b:CProp) => (B_Cases (Equal (X:=CProp)) x a b):CProp).

 

Lemma B_Cases_inv :
  forall (x1 x2 : CProp) (a b : CProp),  (BEqual x1 x2) ->   (BEqual (B_Cases0 x1 a b) (B_Cases0 x2 a b)).
Proof.
intros x1 x2 a b H.
simpl in |- *.
apply B_Decide with x1.
intros.
apply B_Decide with x2.
intros.
apply B_Trans with a.
unfold B_Cases0.
simpl in |- *.
apply B_TrueCase.
assumption.
apply B_Refl.
apply B_Sym.
unfold B_Cases0.
simpl in |- *.
apply B_TrueCase.
assumption.
apply B_Refl.
intros.
apply Contradiction.
apply B_Replace with true.
apply B_Trans with x2.
apply B_Trans with x1.
apply B_Sym.
assumption.
assumption.
assumption.
apply Tautology.
intros.
apply B_Decide with x2.
intros.
apply Contradiction.
apply B_Replace with true.
apply B_Trans with x1.
apply B_Trans with x2.
apply B_Sym.
assumption.
apply B_Sym.
assumption.
assumption.
apply Tautology.
intros.
apply B_Trans with b.
unfold B_Cases0.
simpl in |- *.
apply B_FalseCase.
assumption.
apply B_Refl.
apply B_Sym.
unfold B_Cases0.
simpl in |- *.
apply B_FalseCase.
assumption.
apply B_Refl.
Qed.