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!
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.