Proof with multiple cases theorem

user_17136124 0
Viewed 76

I have a hypothesis of the form

H := check_smaller_thm 1 2 : {2 <= 1} + {2 > 1}

I also have a sub goal

If check_smaller_thm 1 2 then some stuff else some other stuff

I am stuck at this point because I do not see what tactic to use in order to modify H such that I keep the correct Hypothesis (here, {2 > 1}). Then I would like to use it in my sub goal to keep the correct part of the if.

Is there a way to achieve this ?

EDIT

It seems that

If check_smaller_thm 1 2 then some stuff else some other stuff

always applies some stuff instead of other stuff. Is that possible ?

coq proof
2 Answers
user_143149440

If your theorem check_smaller_thm 1 2 has type {2 <= 1} + {2 > 1}, when you type the tactic destruct (check_smaller_thm 1 2), it creates two goals.

One of these goals contains the hypothesis 2 <= 1. This goal says, if 2 was smaller than or equal to 1, then the result would be some_stuff.

So it does look like the if expression returns some_stuff, but it is under a false hypothesis. You can get rid of this goal by showing that this hypothesis is inconsistent.

Here is an example. Notice that we spend some time working on the hypothesis named c2le1. Here I use elementary tactics to solve the problem, but lia would take care of the problem right away.

Require Import Arith Lia.

Lemma tutu (A : Type) (some_stuff : A) (some_other_stuff : A)
  (check_smaller_thm : forall n m, {m <= n}+{m > n}) :
(if check_smaller_thm 1 2 then some_stuff else some_other_stuff)  = some_other_stuff.
Proof.
destruct check_smaller_thm as [c2le1 | c1lt2].
  apply le_S_n in c2le1; inversion c2le1.
reflexivity.
Qed.
user_18092110
Related