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!

Altocumulus

Your question is very difficult to understand. What is arith? where does it come from? In your English text, you write that c and x have different types, but for the if then else statement to be well typed they need to have the same type. – Hertahertberg

@Yves: Edited the question. I just wanted to keep my question simple without having too many definitions atop. – Altocumulus

I am still missing where the notation "a == b" comes from. This notation does not seem to be introduced in the String library from Coq. On the other hand, that library has a sting_dec function. Is it what you use? – Hertahertberg

@Yves. Yes, I used the string_dec function. – Altocumulus

Please post self-contained (including relevant imports), valid code when you ask a question. This doesn't even parse. – Coincidentally

@gallais: I wanted to get an idea without putting too much complexity into the question. Two of the fellow members understood and got back. Kindly don't downvote a question unless it's the only option you have. – Altocumulus

It wouldn't add any complexity to it, quite the contrary. Case in point: you had to answer 2 additional questions to clarify what it was that you wanted to know. – Coincidentally

Interestingly enough, there is the [mcve] shorthand for this link: minimal reproducible example. This means it's a common problem here. I think your question would only become better if you provided a self-contained example. – Mommy

Answer 1

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.

This will generate two goals. In the first one, you will have an hypothesis

hyp_ab : a == b = true

that asserts that the test succeeds and the goal conclusion has the following shape (the if-then-else is replaced by the then branch):

fun c <= S (fun c)

In the second goal, you will have an hypothesis

hyp_ab : a == b = false

and the goal conclusion has the following shape (the if-then-else is replaced by the else branch).

fun x <= S (fun 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 {a = b}+{a <> b}. 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].

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.

Hertahertberg

Thanks a lot. I was looking exactly for case_eq. I really appreciate your detailed explanation. :) – Altocumulus

Answer 2

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.

Quintanilla

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. – Jaconet

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. – Quintanilla