Используйте тактику перезаписи с моим собственным оператором == в Coq - PullRequest
Новая
       14

Используйте тактику перезаписи с моим собственным оператором == в Coq

2 голосов
/ 12 мая 2019

Я пытаюсь доказать простые свойства поля непосредственно из аксиом поля. После некоторых экспериментов с нативной полевой поддержкой Coq ( как этот ) я решил, что лучше просто записать 10 аксиом и сделать их самодостаточными. Я столкнулся с трудностью, когда мне нужно было использовать rewrite с моим собственным оператором ==, который, естественно, не работал. Я понимаю, что должен добавить несколько аксиом, что мои == рефлексивны, симметричны и транзитивны, но мне было интересно, хватит ли этого? или, может быть, есть еще более простой способ использования rewrite с пользовательским ==? Вот мой код Coq: 

Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (opposite: F -> F).
Variable (inverse : F -> F).
Variable (eq: F -> F -> Prop).

Axiom add_assoc: forall (a b c : F), (eq (add (add a b) c) (add a (add b c))).
Axiom mul_assoc: forall (a b c : F), (eq (mul (mul a b) c) (mul a (mul b c))).

Axiom add_comm : forall (a b : F), (eq (add a b) (add b a)).
Axiom mul_comm : forall (a b : F), (eq (mul a b) (mul b a)).

Axiom distr1 : forall (a b c : F), (eq (mul a (add b c)) (add (mul a b) (mul a c))).
Axiom distr2 : forall (a b c : F), (eq (mul (add a b) c) (add (mul a c) (mul b c))).

Axiom add_id1 : forall (a : F), (eq (add a zero) a).
Axiom mul_id1 : forall (a : F), (eq (mul a  one) a).
Axiom add_id2 : forall (a : F), (eq (add zero a) a).
Axiom mul_id2 : forall (a : F), (eq (mul one  a) a).

Axiom add_inv1 : forall (a : F), exists b, (eq (add a b) zero).
Axiom add_inv2 : forall (a : F), exists b, (eq (add b a) zero).

Axiom mul_inv1 : forall (a : F), exists b, (eq (mul a b) one).
Axiom mul_inv2 : forall (a : F), exists b, (eq (mul b a) one).

(*******************)
(* Field notations *)
(*******************)
Notation "0" := zero.
Notation "1" :=  one.
Infix    "+" :=  add.
Infix    "*" :=  mul.
(*******************)
(* Field notations *)
(*******************)
Infix "==" := eq (at level 70, no associativity).

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  specialize add_id1 with (0 * v).
  intros H.

На данный момент у меня есть предположение H : 0 * v + 0 == 0 * v и цель 0 * v == 0. Когда я попытался rewrite H, это, естественно, не удается.

Ответы [ 2 ]

4 голосов
/ 12 мая 2019

Для обобщенного переписывания (перезаписи с произвольными отношениями):

  1. Import Setoid (который загружает плагин, который переопределяет тактику rewrite).

  2. Объявите ваше отношение как отношение эквивалентности (технически rewrite также работает с более слабыми предположениями, скажем, только с транзитивными, но на шаге 3 вам также потребуется работать с гораздо более тонкой иерархией отношений).

  3. Объявите ваши операции (add, mul и т. Д.) Как уважительные этой операции (например, добавление эквивалентных значений должно привести к эквивалентным значениям).Для этого также требуется модуль Morphism.

Вам необходимо выполнить шаг 3, чтобы переписать подвыражения. 

Require Import Setoid Morphisms.

(* eq, add, etc. *)

Declare Instance Equivalence_eq : Equivalence eq.
Declare Instance Proper_add : Proper (eq ==> eq ==> eq) add.
Declare Instance Proper_mul : Proper (eq ==> eq ==> eq) mul.
(* etc. *)

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  specialize add_id1 with (0 * v).
  intros H.
  rewrite <- H. (* Rewrite toplevel expression (allowed by Equivalence_eq) *)
  rewrite <- H. (* Rewrite subexpression (allowed by Proper_add and Equivalence_eq) *)
0 голосов
/ 12 мая 2019

Вот полное решение, основанное на @ Li-yao Xia, в случае, если другие пользователи могут извлечь из этого пользу: 

(***********)
(* IMPORTS *)
(***********)
Require Import Setoid Morphisms.

Variable (F:Type).
Variable (zero:F).
Variable (one :F).  
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (opposite: F -> F).
Variable (inverse : F -> F).
Variable (eq: F -> F -> Prop).

Axiom add_assoc: forall (a b c : F), (eq (add (add a b) c) (add a (add b c))).
Axiom mul_assoc: forall (a b c : F), (eq (mul (mul a b) c) (mul a (mul b c))).

Axiom add_comm : forall (a b : F), (eq (add a b) (add b a)).
Axiom mul_comm : forall (a b : F), (eq (mul a b) (mul b a)).

Axiom distr1 : forall (a b c : F), (eq (mul a (add b c)) (add (mul a b) (mul a c))).
Axiom distr2 : forall (a b c : F), (eq (mul (add a b) c) (add (mul a c) (mul b c))).

Axiom add_id1 : forall (a : F), (eq (add a zero) a).
Axiom mul_id1 : forall (a : F), (eq (mul a  one) a).
Axiom add_id2 : forall (a : F), (eq (add zero a) a).
Axiom mul_id2 : forall (a : F), (eq (mul one  a) a).

Axiom add_inv1 : forall (a : F), exists b, (eq (add a b) zero).
Axiom add_inv2 : forall (a : F), exists b, (eq (add b a) zero).

Axiom mul_inv1 : forall (a : F), exists b, (eq (mul a b) one).
Axiom mul_inv2 : forall (a : F), exists b, (eq (mul b a) one).

(*******************)
(* Field notations *)
(*******************)
Notation "0" := zero.
Notation "1" :=  one.
Infix    "+" :=  add.
Infix    "*" :=  mul.
(*******************)
(* Field notations *)
(*******************)
Infix "==" := eq (at level 70, no associativity).

(****************)
(* eq, add, mul *)
(****************)
Declare Instance Equivalence_eq : Equivalence eq.
Declare Instance Proper_add : Proper (eq ==> eq ==> eq) add.
Declare Instance Proper_mul : Proper (eq ==> eq ==> eq) mul.

(**********************)
(* forall v, 0*v == 0 *)
(**********************)
Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  assert(0 * v == 0 * v + 0) as H1.
  { specialize add_id1 with (0 * v). intros H1. rewrite H1. reflexivity. }
  rewrite H1.
  specialize add_inv1 with (0 * v). intros H2. destruct H2 as [minus_0_v H2].
  assert (0 * v + 0 == 0 * v + (0 * v + minus_0_v)) as H3.
  { rewrite H2. reflexivity. }
  rewrite H3.
  assert ((0 * v + (0 * v + minus_0_v)) == ((0 * v + 0 * v) + minus_0_v)) as H4.
  { specialize add_assoc with (a:=0*v) (b:= 0*v) (c:=minus_0_v). intros H4. rewrite H4. reflexivity. }
  rewrite H4.
  assert (0 * v + 0 * v == (0 + 0) * v) as H5.
  { specialize distr2 with (a:=0) (b:=0) (c:=v). intros H5. rewrite H5. reflexivity. }
  rewrite H5.
  assert (0 + 0 == 0) as H6.
  { specialize add_id1 with (a:=0). intros H6. assumption. } 
  rewrite H6.
  assumption.
Qed.
...