Как доказать равенство из равенства некоторых - PullRequest
Новая
       71

Как доказать равенство из равенства некоторых

0 голосов
/ 19 февраля 2020

Я хочу доказать равенство двух натуральных чисел в Coq: 

a, b : nat
Heq : Some a = Some b
============================
a = b

Ответы [ 3 ]

2 голосов
/ 19 февраля 2020

congruence tacti c достаточно мощный, чтобы решить эту задачу самостоятельно. В более общем случае существуют ситуации, когда вы хотите получить a = b в качестве дополнительной гипотезы, начиная с равенства H : x = y членов, начинающихся с одного и того же конструктора. В этом случае вы можете позвонить 

injection H.

, чтобы извлечь равенства, вытекающие из этой гипотезы.

2 голосов
/ 19 февраля 2020

Когда у вас есть такое равенство, обычно самый быстрый путь к go - это использование inversion tacti c, которое будет более или менее использовать инъекцию конструкторов. 

Lemma foo :
  forall (a b : nat),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e. inversion e. reflexivity.
Qed.

Однако случай Some достаточно особенный, поэтому вы можете написать его по-другому (особенно если вы хотите прочитать сгенерированное доказательство). Вы можете написать некоторую get функцию для option, используя значение по умолчанию: 

Definition get_opt_default {A : Type} (x : A) (o : option A) :=
  match o with
  | Some a => a
  | None => x
  end.

Так что get_opt_default x (Some a) = a. Теперь, используя f_equal (get_opt_default a) на равенстве Some a = Some b, вы получите 

get_opt_default a (Some a) = get_opt_default a (Some b)

, который упрощается до 

a = b

Lemma Some_inj :
  forall A (a b : A),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e.
  apply (f_equal (get_opt_default a)) in e.
  cbn in e.
  exact e.
Qed.

Это то, что можно сделать в целом. По сути, вы пишете экстрактор для вашего значения как функцию и применяете его к обеим сторонам равенства. Вычислением он даст ожидаемый результат.

1 голос
/ 19 февраля 2020

Я думаю, что поучительно написать основную лемму c: 

Definition some_inj A (x y : A) (h_eq : Some x = Some y) : x = y :=
  match h_eq with
  | eq_refl _ => eq_refl
  end.

На самом деле, это кажется удивительным; действительно, Coq разрабатывает совпадение, чтобы помочь пользователю, и реальность немного уродливее, о чем свидетельствует термин: 

Print some_inj.

Definition some_inj A (x y : A) (h_eq : Some x = Some y) : x = y :=
  match h_eq in (_ = option_y)
        return match option_y with
               | Some y => x = y
               | None => IDProp
               end
  with
  | eq_refl => eq_refl
  end.

Так что действительно, тип возвращаемого значения совпадения делает довольно много работы сказать Coq, что конструктор инъективен.

...