1
$\begingroup$

I have the following definitions:

Variables Sd_pre : nat -> Prop.

Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
Admitted.

And the following are two of my hypotheses, which form a contradiction that I am trying to prove:

HeqSd1 : Sd1 = (if Sd_dec m then 0 else 1) 
T_tN_2 : Sd1 = 2

What I tried so far was proving this Lemma, but it didn't help because it was only for bools:

Lemma if_eq: forall d: bool, forall a b c: nat,  (a = if d then b else c) -> if d then a = b else a = c.
Proof.
intros.
induction d. auto. auto.
Qed.

If I try the same for sumbool, I get the error

The term "sumbool" has type "Prop -> Prop -> Set"
which should be Set, Prop or Type.

How do I get this Lemma for sumbool, or is there an easier way?

The same applies to this Lemma that I suppose I will also need to prove my original problem but has the same issue of being defined for bool instead of sumbool.

Lemma if_implies_or: forall a:bool, forall b c : Prop, (if a then b else c) -> b \/ c.
Proof.
intros.
induction a.
auto. auto.
Qed.
$\endgroup$
1
  • $\begingroup$ I was able to solve the original problem with induction tactic over Sd_dec m but I think an answer could still be interesting and valuable learning. $\endgroup$
    – kutschkem
    Commented Jul 2 at 15:15

1 Answer 1

1
$\begingroup$

You can prove it like this:

Section foo.
  Variables Sd_pre : nat -> Prop.
  Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
  Admitted.

  Lemma the_contradiction m Sd1 :
    Sd1 = (if Sd_dec m then 0 else 1) ->
    Sd1 = 2 ->
    False.
  Proof.
    intros -> H. destruct (Sd_dec m). all: discriminate H.
  Qed.
End foo.

The main idea is to do a case distinction on which side of the if we are on. For this, we destruct Sd_dec m and are left with two cases, both of which are contradictory.

Note that the lemma statement for your if_eq would likely be something like

Lemma if_eq {T1 T2}: forall d: sumbool T1 T2, forall a b c: nat,  (a = if d then b else c) -> if d then a = b else a = c.

In particular, sumbool is not a type, but sumbool T1 T2 (with T1, T2 : Prop) is.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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