Докажите неравенство сложных объектов

Question

У меня есть пара карт, которые тривиально несовместимы. Мне интересно, какой изящный / автоматизированный способ получить доказательство этого.

Require Import Coq.Strings.String.

(* Prelude: the total_map data structure from Software Foundations, slightly modified *)
Definition total_map := string -> nat.
Definition empty_st : total_map := (fun _ => 0).
Definition t_update (m : total_map) k v := fun k' => if string_dec k k' then v else m k'.
Notation "a '!->' x" := (t_update empty_st a x) (at level 100).
Notation "x '!->' v ';' m" := (t_update m x v) (at level 100, v at next level, right associativity).

(* The actual goal I'm trying to solve *)
Definition X: string := "X".
Definition Y: string := "Y".
Goal forall n, (X !-> n; Y !-> n) <> (X !-> 1; Y !-> 2).
Proof.
  intros n contra.
  remember (X !-> n; Y !-> n) as st.
  remember (st X) as n1.
  assert (n1 = n). { rewrite Heqn1; rewrite Heqst; cbv; reflexivity. }
  assert (n1 = 1). { rewrite Heqn1; rewrite contra; cbv; reflexivity. }
  remember (st Y) as n2.
  assert (n2 = n). { rewrite Heqn2; rewrite Heqst; cbv; reflexivity. }
  assert (n2 = 2). { rewrite Heqn2; rewrite contra; cbv; reflexivity. }
  congruence.
Qed.

Answer 1

Чтобы автоматизировать это, вам нужно иметь точное описание вашей стратегии доказательства. Вот одна из возможных стратегий доказательства:

Для доказательства неравенства total_map с:

1. Сначала представьте гипотезу равенства.
2. Затем для каждого ключа, добавленного на любую карту, добавьте гипотезу о том, что значение, связанное с этим ключом, одинаково на обеих картах.
3. Затем упростите все такие гипотезы равенства, развернув t_update, используя для этого значение string_dec x x и посмотрев, вычисляются ли другие string_dec s.
4. Наконец, решите цель с помощью congruence.

Мы можем автоматизировать каждый из этих шагов. Всего становится:

Require Import Coq.Strings.String.

(* Prelude: the total_map data structure from Software Foundations, slightly modified *)
Definition total_map := string -> nat.
Definition empty_st : total_map := (fun _ => 0).
Definition t_update (m : total_map) k v := fun k' => if string_dec k k' then v else m k'.
Notation "a '!->' x" := (t_update empty_st a x) (at level 100).
Notation "x '!->' v ';' m" := (t_update m x v) (at level 100, v at next level, right associativity).

(* Automation *)

(* 1. First introduce the equality hypothesis. *)
Ltac start_proving_inequality H :=
  intro H.

(* 2. Then, for every key that's been added to either map, add the hypothesis that the value associated to that key is the same in both maps. *)
(* To do this, we need a tactic that will pose a proof only if it does not already exist. *)
Ltac unique_pose_proof lem :=
  let T := type of lem in
  lazymatch goal with
  | [ H : T |- _ ] => fail 0 "A hypothesis of type" T "already exists"
  | _ => pose proof lem
  end.

(* Maybe move this elsewhere? *)
Definition t_get (m : total_map) k := m k.

Ltac saturate_with_keys H :=
  repeat match type of H with
         | context[t_update _ ?k ?v]
           => unique_pose_proof (f_equal (fun m => t_get m k) H)
         end.

(* 3. Then simplify all such equality hypotheses by unfolding `t_update`, using that `string_dec x x` is true, and seeing if any other `string_dec`s compute down. *)
Require Import Coq.Logic.Eqdep_dec.
Lemma string_dec_refl x : string_dec x x = left eq_refl.
Proof.
  destruct (string_dec x x); [ apply f_equal | congruence ].
  apply UIP_dec, string_dec.
Qed.

(* N.B. You can add more cases here to deal with other sorts of ways you might reduce [t_get] here *)
Ltac simplify_t_get_t_update_in H :=
  repeat first [ progress cbv [t_get t_update empty_st] in H
               | match type of H with
                 | context[string_dec ?x ?x] => rewrite (string_dec_refl x) in H
                 | context[string_dec ?x ?y]
                   => let v := (eval cbv in (string_dec x y)) in
                      (* check that it fully reduces *)
                      lazymatch v with left _ => idtac | right _ => idtac end;
                      progress change (string_dec x y) with v in H
                 end ].

Ltac simplify_t_get_t_update :=
  (* first we must change hypotheses of the form [(fun m => t_get m k) m = (fun m => t_get m k) m'] into [t_get _ _ = t_get _ _] *)
  cbv beta in *;
  repeat match goal with
         | [ H : t_get _ _ = t_get _ _ |- _ ] => progress simplify_t_get_t_update_in H
         end.

(* 4. Finally, solve the goal by `congruence`. *)
Ltac finish_proving_inequality := congruence.

(* Now we put it all together *)
Ltac prove_total_map_inequality :=
  let H := fresh in
  start_proving_inequality H;
  saturate_with_keys H;
  simplify_t_get_t_update;
  finish_proving_inequality.

(* The actual goal I'm trying to solve *)
Definition X: string := "X".
Definition Y: string := "Y".
Goal forall n, (X !-> n; Y !-> n) <> (X !-> 1; Y !-> 2).
  intros.
  prove_total_map_inequality.
Qed.

Answer 2

Исходя из ответа Джейсона Гросса и того факта, что total_map является решающим типом, я собрал немного автоматизации, чтобы справиться с этим. Обратите внимание, что эта проблема, вероятно, очень хорошо подходит для мелкомасштабного отражения.

(* TODO: don't bring trivial (n = n) or duplicated hypotheses into scope *)

(* Given two maps left and right, plus a lemma that they are equal, plus some key: assert that the values of the maps agree at the specified key *)
Ltac invert_total_map_equality_for_id lemma left right id :=
  let H := fresh "H" in
  assert (left id = right id) as H by (rewrite lemma; reflexivity); 
  cbv in H.

(* Recurse on the LHS map, extracting keys *)
Ltac invert_total_map_equality_left lemma left right left_remaining :=
  match left_remaining with
  | t_update ?left_remaining' ?id _ =>
    invert_total_map_equality_for_id lemma left right id;
    invert_total_map_equality_left lemma left right left_remaining'
  | _ => idtac
  end.

(* Recurse on the RHS map, extracting keys; move on to LHS once we've done all RHS keys *)
Ltac invert_total_map_equality_right lemma left right right_remaining :=
  match right_remaining with
  | t_update ?right_remaining' ?id _ =>
    invert_total_map_equality_for_id lemma left right id;
    invert_total_map_equality_right lemma left right right_remaining'
  | _ => invert_total_map_equality_left lemma left right left
  end.

(* Given a lemma that two total maps are equal, assert that their values agree at each defined key *)
Ltac invert_total_map_equality lem :=
  let T := type of lem in
    match T with
    | ?left = ?right =>
      match type of left with
      | string -> nat =>
        match type of right with
        | string -> nat =>
          invert_total_map_equality_right lem left right right
      end
    end
  end.

Goal forall n, (X !-> n; Y !-> n) <> (X !-> 1; Y !-> 2).
Proof.
  unfold not; intros.
  invert_total_map_equality H.
  congruence.
Qed.