Я запутался в доказательствах и Prop и т. д. в Coq. Как мы докажем, что (n = n) = (m = m)?
Я намерен показать, что это как-то True=True. Но это даже правильная формулировка?
Что я пробовал до сих пор:
Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.
Но simpl. ничего не делает, и reflexivity тоже. Это просто пример, в общем мне нужно доказать это для любого типа X если это возможно.
n = n и m = m являются предложениями, поэтому они относятся к типу Prop, а не к типу Set. По сути, это означает, что n = n похоже на утверждение (которое нужно доказать), а не что-то вроде true : boolean.
Вместо этого вы можете попробовать доказать что-то вроде: n-n = m-m, или вы можете определить функцию nat_equal : nat -> bool, которая при заданном натуральном значении сопоставляет его с bool, а затем доказать nat_equal n = nat_equal m.
Если вы действительно хотите утверждать, что утверждения равны, вам понадобится пропозициональная экстенсиональность.
невозможно доказать то, о чем вы просите, без принятия дополнительных аксиом; ср. этот ответ .
(n = n) <-> (m = m)? Поскольку<->можно рассматривать как равенство между предложениями, в Coq. - person Rodrigo Ribeiro schedule 08.12.2015n = mи такrefl n <> refl m. Я потратил последний час, пытаясь доказать, что(a=a)=(b=b)терпит неудачу, еслиa<>b, но все еще застрял. Я попробовал несколько интересных подходов и, возможно, опубликую ответ позже с подробным описанием того, почему то, что я пробовал, должно потерпеть неудачу. (Но сейчас у меня просто голова болит…) - person nobody schedule 08.12.2015