我有一对平凡不兼容的地图。我想知道什么是优雅/自动化的方式来获得它的证明。
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.
为了使其自动化，您需要准确描述您的证明策略。这是一种可能的证明策略：
为了证明total_maps的不平等：
t_update来简化所有这些相等假设，使用string_dec x x为真，并查看是否有任何其他string_decs计算下来。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.
基于Jason Gross的回答以及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.