coq tactic - 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.

Thanks!

Answer 1

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.

Variables (T : eqType) (a b : T).
Lemma u : (if a == b then 0 else 1) = 2.
Proof.

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:

Inductive 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

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.
Goal 1: (a == b) = true  -> 0 = 2
Goal 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.

you'll get:

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

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