Пролог
Думаю, вы хотите доказать, что конкатенация векторов ассоциативна, а затем использовать этот факт как лемму.
Но 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
выглядит немного проще, чем предыдущие.
Другие подходы к векторам
См., Например, этот вопрос и этот < / а>; Я также считаю очень полезным этот ответ.
person
Anton Trunov
schedule
13.05.2018