How to pattern match on a boolean equality on strings and simultaneously gain the desired propositional equality in a proof in Coq?

Question

I'm getting stuck trying to prove the substi_correct theorem in SF because I don't know how to split on boolean equality and simultaneously assert this as propositional equality.

Theorem substi_correct : forall s x t t',
  [x:=s]t = t' <-> substi s x t t'.
Proof.
  intros. 
  split. 
  + generalize dependent t'.
    induction t; intros.
    - simpl in H.
      subst.
      case (eqb_string x0 s0).
      * constructor. (*Doesn't work*)

The proof goal is as follows, without the needed H : x0 = s0 so that I can proceed.

  s : tm
  x0, s0 : string
  ============================
  substi s x0 (var s0) s

In the Maps.v chapter we prove, in addition to a false case,

Theorem eqb_string_true_iff : forall x y : string,
    eqb_string x y = true <-> x = y.

but how can I use then when pattern matching on (eqb_string x0 s0) so that I can proceed? Am I supposed to use this as a lemma in the proof or is there an easier way to proceed?

Answer 1

You can use the variant of the destruct tactic with the eqn: clause to add a hypothesis remembering which case you're in:

  destruct (eqb_string x0 s0) eqn:Ex0s0  (* <-- You can pick any name for the equation here *)
  - (* Ex0s0 : eqb_string x0 s0 = true *)
    apply eqb_string_true_iff in Ex0s0.
    ...
  - (* Ex0s0 : eqb_string x0 s0 = false *)
    apply eqb_string_false_iff in Ex0s0.
    ...