CODEWITHSUNDEEP
coq
user1953221
user1953221

Reputation: 429

Case splitting on if-then-else condition

This is a silly beginner question, but how do I prove this theorem?

Open Scope Z.
Theorem test : forall x y:Z, (x > 0 -> y = 1) \/ (x <= 0 -> y = 2) -> y >= 1.
Proof.
  intros.
  destruct x.
  destruct H.
  (* stuck *)
Qed.

What I'm really trying to do is model an if-then-else statement as a Prop and case split on the condition to prove it. I get stuck with the context like this:

y: nat
H: 0 > 0 -> y = 1
-----------------
(1/3)
y >= 1
(2/3)
y >= 1
(3/3)
y >= 1

I sort of understand that to get rid of impossible cases, I need to find a contradiction in the hypothesis, but how do I do that here?

Advice on how this could be done better is welcome, e.g. is this the best way to model if-then-else?

Upvotes: 1

Views: 588

Answers (2)

larsr
larsr

Reputation: 5811

how do I prove this theorem?

Theorem test : forall x y:Z, (x > 0 -> y = 1) \/ (x <= 0 -> y = 2) -> y >= 1.

Your theorem is not true.

Suppose H: x > 0 -> y = 1 but x is actully 0, then you have no way of proving y >= 1 as you know nothing about y.

Perhaps you meant to use and (/\) instead of or? Then here's one proof that uses lia to do the tedious Z arithmetic.

Require Import ZArith Lia. Open Scope Z.
Theorem test : forall x y:Z, (x > 0 -> y = 1) /\ (x <= 0 -> y = 2) -> y >= 1.
Proof.  intros x y [H1 H2]. enough (x>0 \/ x<=0) as [H|H]; lia. Qed.

Upvotes: 1

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

I think what you are looking for is the lemma

Z_lt_le_dec : forall x y : Z, {x < y} + {y <= x}

of the library. What { … } + { … } means is similar to \/, i.e. it is a kind of disjuction, but here this disjuction constructs a type in Set rather than Prop. This means that while you cannot use a \/ disjuction to build a function returning a nat (because of Coq’s enforcement that propositions should be irrelevant) you can use a { … } + { … } one. You can write

Definition test (x : Z) := if (Z_lt_le_dec 0 x) then 1 else 2.

which is syntactic sugar for a pattern matching like this one

Definition test (x : Z) := match (Z_lt_le_dec 0 x) with
  | left _ => 1
  | right _ => 2
end.

where left and right are the two constructors of { … } + { … }.

To check that this test does what it should, you can now try to go and prove

Lemma test_ge1 (x : Z) : 1 <= test x.

Upvotes: 1

Related Questions