Применение определения программы завершается с ошибкой «невозможно объединить опору с [целью]» - PullRequest
Новая
       7

Применение определения программы завершается с ошибкой «невозможно объединить опору с [целью]»

0 голосов
/ 13 мая 2018

В Coq я показал ассоциативность append на векторах, используя: 

Require Import Coq.Vectors.VectorDef Omega.
Program Definition t_app_assoc v p q r (a : t v p) (b : t v q) (c : t v r) :=
  append (append a b) c = append a (append b c).
Next Obligation. omega. Qed.

Теперь я хочу применить это равенство в доказательстве.Ниже приведена самая легкая цель, которую я ожидал бы получить с помощью t_app_assoc.Конечно, это может быть подтверждено simpl - это всего лишь пример. 

Goal (append (append (nil nat) (nil _)) (nil _)
   = append (nil _) (append (nil _) (nil _))).
apply t_app_assoc.

Этот apply завершается неудачно с:

Ошибка: невозможно объединить "Prop"с
"append (append (nil nat)) (nil nat)) (nil nat) =
append (nil nat) (append (nil nat) (nil nat))".

Как я могу применить t_app_assoc?Или есть лучший способ определить это?Я думал, что мне нужен Program Definition, потому что простое использование Lemma приводит к ошибке типа, потому что t v (p + (q + r)) и t v (p + q + r) не совпадают с Coq.

1 Ответ

0 голосов
/ 13 мая 2018

Пролог

Полагаю, вы хотите доказать, что конкатенация векторов ассоциативна, а затем использовать этот факт в качестве леммы.

Но t_app_assoc, как вы определяете, имеет следующий тип: 

t_app_assoc
     : forall (v : Type) (p q r : nat), t v p -> t v q -> t v r -> Prop

Вы в основном хотите использовать : вместо := следующим образом. 

From Coq Require Import Vector Arith.
Import VectorNotations.
Import EqNotations.  (* rew notation, see below *)

Section Append.

Variable A : Type.
Variable p q r : nat.
Variables (a : t A p) (b : t A q) (c : t A r).

Fail Lemma t_app_assoc :
  append (append a b) c = append a (append b c).

К сожалению, мы не можем даже сформулировать такую ​​лемму, используя обычное однородное равенство.

Левая сторона имеет следующий тип: 

Check append (append a b) c : t A (p + q + r).

, тогда как правая сторона имеет тип 

Check append a (append b c) : t A (p + (q + r)).

Поскольку t A (p + q + r) не совпадает с t A (p + (q + r)), мы не можем использовать = для формулировки приведенной выше леммы.

Позвольте мне описать некоторые способы решения этой проблемы:

rew обозначение 

Lemma t_app_assoc_rew :
  append (append a b) c = rew (plus_assoc _ _ _) in
  append a (append b c).
Admitted.

Здесь мы просто используем закон ассоциативности сложения для натуральных чисел, чтобы привести тип RHS к t A (p + q + r).

Чтобы это заработало, нужно Import EqNotations. до этого.

cast функция

Это распространенная проблема, поэтому авторы библиотеки Vector решили предоставить функцию cast следующего типа: 

cast :
  forall (A : Type) (m : nat),
  Vector.t A m -> forall n : nat, m = n -> Vector.t A n

Позвольте мне показать, как его можно использовать для доказательства закона ассоциативности векторов. Но сначала докажем следующую вспомогательную лемму: 

Lemma uncast {X n} {v : Vector.t X n} e :
  cast v e = v.
Proof. induction v as [|??? IH]; simpl; rewrite ?IH; reflexivity. Qed.

Теперь все готово: 

Lemma t_app_assoc_cast (a : t A p) (b : t A q) (c : t A r) :
  append (append a b) c = cast (append a (append b c)) (plus_assoc _ _ _).
Proof.
  generalize (Nat.add_assoc p q r).
  induction a as [|h p' a' IH]; intros e.
  - now rewrite uncast.
  - simpl; f_equal. apply IH.
Qed.

Гетерогенное равенство (например, равенство Джона Мейджора) 

Lemma t_app_assoc_jmeq :
  append (append a b) c ~= append a (append b c).
Admitted.

End Append.

Если вы сравните определение однородного равенства 

Inductive eq (A : Type) (x : A) : A -> Prop :=
  eq_refl : x = x.

и определение гетерогенного равенства 

Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
  JMeq_refl : x ~= x.

вы увидите, что с JMeq LHS и RHS не обязательно должны быть одного типа, и поэтому выражение t_app_assoc_jmeq выглядит немного проще, чем предыдущие.

Другие подходы к векторам

Смотри, например, этот вопрос и этот ; Я также нахожу этот ответ тоже очень полезно.

...