Как сопоставить шаблон на булевом равенстве на строках и одновременно получить желаемое пропозициональное равенство в доказательстве в Coq?

Question

Я застреваю, пытаясь доказать теорему substi_correct в SF, потому что я не знаю, как разделить логическое равенство и одновременно утверждать это как пропозициональное равенство.

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*)

Целью доказательства является далее, без необходимой H: x0 = s0, чтобы я мог продолжить.

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

В главе Maps.v мы доказываем, помимо ложного случая,

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

но как я могу использовать тогда, когда сопоставление с образцом (eqb_string x0 s0), чтобы я мог продолжить? Я должен использовать это как лемму в доказательстве или есть более простой способ продолжить?

Answer 1

Вы можете использовать вариант destruct tacti c с предложением eqn:, чтобы добавить гипотезу о том, в каком случае вы находитесь:

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