1
$\begingroup$

In Coq, I made some record structure $I$ and also make a strict order and equality $<$ and $==$.

And I showed that $a < b$ or $a == b$ or $b < a$ for every $a, b \in I$.

forall a b : I, a < b \/ a == b \/ b < a

Since my construction is not decidable, I use an decidable axiom.

Axiom I_dec : forall a b : I, {a < b} + {a == b} + {b < a}.

I want to use this axiom in case analysis. However, I cannot deal with all three cases.

For example,

Example example : 
forall a b : I, if (I_dec a b) then a < b else True. 
Proof.
intros. destruct (I_dec a b) as [[H|H]|H]. 
{ simpl. exact H. }
{ simpl.

I want to reach only the most left case $a < b$, however it is impossible for me.

Is there a way to deal with all three cases respectively?

$\endgroup$

1 Answer 1

1
$\begingroup$

Probably a problem with notations, incompatible with your use of if. Let's have a look at I_dec's structure (I set I = nat).

Unset Printing Notations.
Check I_dec. 

I_dec
     : forall a b : nat, sumor (sumbool (lt a b) (eq a b)) (lt b a)

The main cases of I_dec a b are (sumbool (lt a b) (eq a b)) and (lt b a).

A possible workaround (among others) is to define a variant of if:

Notation if' t t1 t2 :=
  match t with inleft (left H) => t1 | _ => t2 end.

Example example : 
forall a b : nat, if' (I_dec a b) (a < b) True.
Proof.
intros; destruct (I_dec a b) as [[H | _] | _]; auto.
Qed. 
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.