Чтобы автоматизировать это, вам нужно иметь точное описание вашей стратегии доказательства. Вот одна из возможных стратегий доказательства:
Для доказательства неравенства total_map
с:
- Сначала представьте гипотезу равенства.
- Затем для каждого ключа, добавленного на любую карту, добавьте гипотезу о том, что значение, связанное с этим ключом, одинаково на обеих картах.
- Затем упростите все такие гипотезы равенства, развернув
t_update
, используя для этого значение string_dec x x
и посмотрев, вычисляются ли другие string_dec
s.
- Наконец, решите цель с помощью
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.