Proof if then else function with if hypothesis

Using Coq
1

Hi all, I am beginning with Coq theorem prover and I am stuck at this kind of example (need help).
I have an if_then_else function (fun: if x then Some else None).
And in my proof I have:
-a hypothesis H representing the x condition
-I want to prove that fun = Some
Could you give me key points on how to proceed the proof !?
Thankies
Lil

2

If H is of the form x = true you can rewrite your goal using H (rewrite H.) and the if should reduce itself to Some (cf background below).

If H is some property that only imply x = true then either

  • you first prove x = true and proceed as above,
  • or you first destruct x eqn:heq. You then have 2 subgoals with 2 different equations heq: one is the x = true (proceed as above) and the other is x = false and you should discharge it by contradiction.

Background: if X then A else B is syntactic sugar for match x with true -> A | false -> B end. and it will only reduce if x starts with a constructor (true or false if x is of type bool).

3

Thank you for the quick+useful reply, it allowed me to get started, though I am still a bit stuck, here is the example to give you more context

Record test :={
a: nat;
b: nat
}.
Definition func (s: test) : option test :=
if leb s.(a) s.(b) then
if s.(a) =? s.(b) then Some s
else Some (Build_test 1 2)
else None.

(* This Lemma is here to have H → x=true as you explicited for next proof *)
Lemma Need : forall (s: test), s.(a) <= s.(b) → leb s.(a) s.(b) = true.
Proof.
intros.
apply Nat.leb_le in H.
exact H.
Qed.

(* What I am trying to prove: basically if the condition is fulfilled I have a proper test *)
Lemma trial : forall (s: test), s.(a) <= s.(b) → exists s’, func2 s = Some s’.
Proof.
intros.
assert (H’: forall (s: test), s.(a) <= s.(b) → leb s.(a) s.(b) = true).
{ intros. apply Need. exact H0. }
unfold func2.
rewrite H’.
+

  1. When I use H’, it simplifies func by taking off the second else, but I find myself stuck with the first if-else (equal or strictly lower)
  2. I still don’t know how to handle the exists, because if I try to move it to the context part, it changes the goal to equal Some s1, and it’s not what I want to prove (s not necessarily = s1).

Any clues ?
Thanks again :slight_smile:
Lil

4

Your code does not contain the definition of func2, so it is not quite clear what you are trying to achieve.

By the way, in your messages, please format any Coq script as follows, so that it becomes readable to others:

```coq
Record test :={
  a: nat;
  ...
```

Also, you do not really need the lemma Need in your script. You can directly do

rewrite leb_correct.

and since the condition for the rewrite is already in the context, you can even do

rewrite leb_correct by easy.
5

Hi,
Sorry, typo problem, func2 is actually func (I was just trying a lot of things).

Here is the proof (probably not optimized), hope it is useful for people finding this post.
(**** PROOF *****)

Lemma Need1 : forall (s: test), s.(a) <= s.(b) → leb s.(a) s.(b) = true.
Proof.
intros.
apply Nat.leb_le in H.
exact H.
Qed.

Lemma Need2 : forall (s: test), s.(a) <= s.(b) → (eqb s.(a) s.(b) = true) / (ltb s.(a) s.(b) = true).
Proof.
intros.
destruct (Nat.eqb_spec s.(a) s.(b)) as [Heq | Hneq]. (* Case analysis on a = b *)

  • left.
    reflexivity.
  • right.
    Search (_ <? _ = true) nat.
    apply Nat.ltb_lt.
    Search (_ < ) ( <= ) ( <> _) nat.
    apply Nat.le_neq.
    split.
    • exact H.
    • exact Hneq.
      Qed.

Lemma Need3 : forall (s : test),
(s.(a) <? s.(b)) = true → s.(a) <> s.(b).
Proof.
intros s Hlt Heq.
apply Nat.ltb_lt in Hlt.
rewrite Heq in Hlt.
apply Nat.lt_irrefl in Hlt.
contradiction Hlt.
Qed.

Lemma trial : forall (s: test), s.(a) <= s.(b) → exists s’, func s = Some s’.
Proof.
intros.
assert (H1: s.(a) <= s.(b) → leb s.(a) s.(b) = true).
{ intros. apply Need1. exact H0. }
unfold func2.
rewrite H1.

  • assert (H2: s.(a) <= s.(b) → (eqb s.(a) s.(b) = true) / (ltb s.(a) s.(b) = true)).
    { intros. apply Need2. exact H. }
    destruct H2.
    • exact H.
    • rewrite H0.
      exists s. reflexivity.
    • Search (_ <? _ = true) nat.
      assert (H3: (a s <? b s) = true → a s <> b s).
      { intros. apply Need3. exact H0. }
      apply H3 in H0.
      Search (_ <> _) ( _ =? _ = false) nat.
      apply Nat.eqb_neq in H0.
      rewrite H0.
      exists {| a := 1; b := 2 |}.
      reflexivity.
    • exact H.
      Qed.

Thanks a lot for the guidance !