Пояснение транзитивности равных ко - PullRequest
Новая
       28

Пояснение транзитивности равных ко

0 голосов
/ 17 февраля 2019

У меня есть доказательство, которое уже доказано. 

Lemma Equal_Trans : forall T : Type, forall y x z: T, 
      Equal x y -> Equal y z -> Equal x z.

И, во-вторых, у меня есть исправление доказательства дополнительной коммутативности. 

Lemma Add_com : forall x x': Nat, Equal (Add x x') (Add x' x).
Proof.
intros.
induction x.
simpl.
apply Add_zero.
simpl.
apply (Equal_Trans Nat (S (Add x' x)) ). (* var y *)
apply Equal_Morph.
assumption.
apply Add_S.
Qed.

Однако я не понимаюиспользование Equal_trans (строка 8).Если я понимаю, Equal_Trans принимает 3 аргумента: yxz?Но почему в лемме Add_com используется только 1 аргумент, использующий Equal_Trans?

Заранее благодарю за помощь.

Ответы [ 2 ]

0 голосов
/ 17 февраля 2019

Большое спасибо за помощь.

Если я понимаю, Equal_trans принимает только 1 аргумент, аргумент y?

Но, прежде чем выполнить команду apply (Equal_Trans Nat (S (Add x' x)) ), CoqIDE говорит мне: 

1 subgoal
x, x' : Nat
IHx : Equal (Add x x') (Add x' x)
______________________________________(1/1)
Equal (S (Add x x')) (Add x' (S x))

Я не понимаю, почему здесь я должен взять y: = S (Добавить x 'x) применить Equal_trans?

0 голосов
/ 17 февраля 2019

Тактика apply пытается заполнить пробелы, чтобы тип поставленного термина соответствовал цели.В этом случае цель (когда используется тактика), вероятно, что-то вроде a = b (в зависимости от вашего наблюдения это на самом деле Equal a b).Тип Equal_Trans (когда используются все аргументы) - x = z (Equal x z), поэтому для объединения этих двух типов у нас должны быть x := a и z := b.Из-за этого y остается двусмысленным, поэтому мы должны предоставить его.

Чтобы ответить на ваш вопрос, нет, Equal_Trans не принимает только один аргумент.Он принимает тип (Nat в вашем случае) три элемента этого типа (y, x и z) и два доказательства равенства.Однако помните, что функции в Coq каррируются, что означает, что вы можете вызывать их с меньшим количеством аргументов, но в результате вы получите функцию от оставшихся аргументов.

Так что на самом деле, когда мы говорим apply (Equal_Trans Nat (S (Add x' x))., мыВы говорите: «Возьмите эту вещь с типом forall (x z: Nat), Equal x (S (Add x' x)) -> Equal (S (Add x' x)) z -> Equal x z и попробуйте ввести некоторые аргументы, чтобы она соответствовала моей цели».

Coq смотрит на этот тип и понимает, что цель уже выглядит как Equal x z, так что он может определить, какие x и z должны быть.Equal_Trans все еще принимает еще два аргумента, которые Coq не может выяснить самостоятельно (доказательства Equal x y и Equal y z), так что это то, что делает остальная часть доказательства.

Мы используем транзитивность с y := S (Add x' x), потому что мы можем доказать Equal (S (Add x x')) (S (Add x' x)), используя индуктивную гипотезу (IHx).Мы также можем доказать Equal (S (Add x' x)) (Add x' (S x)), используя определение Add.Следовательно, естественно направить доказательство равенства через S (Add x' x).

Теперь у нас нет для использования транзитивности с y := S (Add x' x).Мы могли бы доказать, что (S (Add x x')) и (Add x' (S x)) оба равны некоторому другому элементу Nat.Но самый простой и прямой маршрут - через S (Add x' x).

...