0
$\begingroup$

I made some record structure $I$ with addition and equality. And I made an axiom.

Axiom I_dec : 
forall a : I, ({0 < a} + {a < 0}) + {a == 0}.

With this axiom, I define a multiplication of $I$.

Definition I_seq_mult_l (a b : I) := 
match (I_dec a) with 
 | inleft (left H) => 
   match (I_dec b) with 
    | inleft (left H) => ...
    | inleft (right H) => ...
    | inright H => ...
   end
 | inleft (right H) => 
   match (I_dec b) with 
    | inleft (left H) => ...
    | inleft (right H) => ...
    | inright H => ...
   end 
 | inright H => ...
end.

When I prove some lemma, I meet an unsolved situation.

1 goal
a, b : I
Ha : const_I 0 < a
Hb : const_I 0 < b
Hb' : - b < const_I 0
______________________________________(1/1)
(exists m : positive,
   forall n : positive,
   (m <= n)%positive ->
   -
   match I_dec (- b) with
   | inleft (left _) => ...
   | inleft (right _) =>
       fun n0 : positive => ...
   | inright _ => ...
   end n <= r a n * r b n)

Previously, I destruct (I_dec a) and (I_dec b).

destruct (I_dec a) as [[Ha|Ha]|Ha], (I_dec b) as [[Hb|Hb]|Hb].

I made a hypothesis Hb' from Hb. And I think Hb' implies that I_dec (- b) match with inleft (right _).

So I want to write 'simpl' and make this goal simple.

However, I can't do this. So, I destruct (I_dec (- b)) also. It multiplies steps three times.

Can I match a processed hypothesis with a part of a decidable axiom?

$\endgroup$

1 Answer 1

1
$\begingroup$

If you think that Hb' implies that I_dec (-b) matches with inleft (right _)… then you should just prove that. Something like

Lemma lt0 {a : I} : a < 0 -> exists p, I_dec a = inleft (right p)

Even better, if you happen to have some uniqueness of proofs, you might prove

Lemma lt0 {a : I} (H : a < 0), I_dec a = inleft (right H)

To prove this, you will probably need extra axioms on <, stating that it is irreflexive and transitive.

In your setting you could then use the lemma, with something like

destruct (lt0 Hb') as [? ->].

This uses the lemma to replace the I_dec (-b) in your goal by inleft (right p) for some variable p you just introduced. Then you can use simpl and have the goal simplified as you hope.

If this situation turns up often (and I guess it will if you have a lot of these definitions around), you might want some automated tactic to do this for you. You could try something like

Lemma lt0 {a : I} : a < 0 -> exists p, I_dec a = inleft (right p).
…

Lemma gt0 {a : I} : 0 < a -> exists p, I_dec a = inleft (left p).
…

Lemma eq0 : exists p, I_dec z = inright p.
…

Ltac simp_dec :=
  repeat (match goal with
    | H : lt ?a z |- context [I_dec ?a] => destruct (lt0 H) as [p ->] ; clear p
    | H : lt z ?a |- context [I_dec ?a] => destruct (gt0 H) as [p ->] ; clear p
    | H : 
    | |- context [I_dec z] => destruct eq0 as [p ->] ; clear p
  end) ; simpl.

This tactic repeatedly replaces the I_dec _ appearing in your terms until there are none left, and simplifies the whole term at the end.

$\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.