Coq: How to prove if statements involving strings?

Question

I have a string a and on comparison with string b, if equals has an string c, else has string x. I know in the hypothesis that fun x <= fun c. How do I prove this below statement? fun is some function which takes in string and returns nat.

fun (if a == b then c else x) <= S (fun c).

The logic seems obvious but I am unable to split the if statements in coq. Any help would be appreciated.

Answer (ejgallego)

Let me complement Yves answer pointing out to a general "view" pattern that works well in many situations were case analysis is needed. I will use the built-in support in math-comp but the technique is not specific to it.

Let's assume your initial goal:

From mathcomp Require Import all_ssreflect.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Variables (T : eqType) (a b : T).
Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Lemma u : (if a == b then 0 else 1) = 2.
(if a == b then 0 else 1) = 2
Proof.
(if a == b then 0 else 1) = 2

now, you could use case_eq + simpl to arrive to next step; however, you can also match using more specialized "view" lemmas. For example, you could use ifP:

ifP
     : forall (A : Type) (b : bool) (vT vF : A),
       if_spec b vT vF (b = false) b
         (if b then vT else vF)

where if_spec is:

Variant
if_spec (A : Type) (b : bool) (vT vF : A)
(not_b : Prop) : bool -> A -> Set :=
    IfSpecTrue : b -> if_spec b vT vF not_b true vT
  | IfSpecFalse : not_b ->
                  if_spec b vT vF not_b false vF

Arguments if_spec [A]%type_scope _%bool_scope _ _
  _%type_scope _%bool_scope _
Arguments IfSpecTrue [A]%type_scope [b]%bool_scope _ _
  _%type_scope _
Arguments IfSpecFalse [A]%type_scope _%bool_scope _ _
  [not_b]%type_scope _

That looks a bit confusing, the important bit is the parameters to the type family bool -> A -> Set. The first exercise is "prove the ifP lemma!".

Indeed, if we use ifP in our proof, we get:

  case: ifP.
a == b -> 0 = 2
(a == b) = false -> 1 = 2
a == b -> 0 = 2
(a == b) = false -> 1 = 2

Note that we didn't have to specify anything! Indeed, lemmas of the form { A } + { B } are just special cases of this view pattern. This trick works in many other situations, for example, you can also use eqP, which has a spec relating the boolean equality with the propositional one. If you do:

  case: eqP.
a = b -> 0 = 2
a <> b -> 1 = 2

you'll get:

a = b -> 0 = 2
a <> b -> 1 = 2

which is very convenient. In fact, eqP is basically a generic version of the type_dec principle.

Q: Where does the name "view" come from and what is the general intuition one should have about views? I mean, they are not rewriting equations or inversion lemmas.

A: I am not sure where does the name "view" come from, likely there are better names, maybe "specification". I call it view as for some operators (ie <=) you have different "views" on the case analysis. The intuition behind a "view" is that it will do case analysis on some construction, populating the context properly as to continue the proof. This is sometimes not trivial and usually saves quite a bit amount of time.

Answer (Yves)

If you can write an if-then-else statement, it means that the test expression a == b is in a type with two constructors (like bool) or (sumbool). I will first assume the type is bool. In that case, the best approach during a proof is to enter the following command.

  case_eq (a == b); intros hyp_ab.
hyp_ab: (a == b) = true
fn c <= S (fn c)
hyp_ab: (a == b) = false
fn x <= S (fn c)

This will generate two goals. In the first one, you will have an hypothesis that asserts that the test succeeds and the goal conclusion has the following shape (the if-then-else is replaced by the then branch):

subgoal 1 is:

  hyp_ab : (a == b) = true
  ============================
  fn c <= S (fn c)

In the second goal, you will have an hypothesis and the goal conclusion has the following shape (the if-then-else is replaced by the else branch).

subgoal 2 is:

  hyp_ab : (a == b) = false
  ============================
  fn x <= S (fn c)

You should be able to carry on from there.

On the other hand, the String library from Coq has a function string_dec with return type

string_dec
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

If your notation a == b is a pretty notation for string_dec a b, it is better to use the following tactic:

  destruct (a == b) as [hyp_ab | hyp_ab].
hyp_ab: a = b
fn c <= S (fn c)
hyp_ab: a <> b
fn x <= S (fn c)

The behavior will be quite close to what I described above, only easier to use.

Intuitively, when you reason on an if-then-else statement, you use a command like case_eq, destruct, or case that leads you to studying separately the two executions paths, remember in an hypothesis why you took each of these executions paths.