Что означает `true = false` в Coq?
Исключение нулевого указателя - это индикатор того, что вы используете объект, не инициализируя его.
Например, ниже - класс ученика, который будет использовать его в нашем коде.
public class Student {
private int id;
public int getId() {
return this.id;
}
public setId(int newId) {
this.id = newId;
}
}
Приведенный ниже код дает вам исключение с нулевым указателем.
public class School {
Student obj_Student;
public School() {
try {
obj_Student.getId();
}
catch(Exception e) {
System.out.println("Null Pointer ");
}
}
}
Поскольку вы используете Obj_Student, но вы забыли инициализировать его, как в правильном коде, показанном ниже:
public class School {
Student obj_Student;
public School() {
try {
obj_Student = new Student();
obj_Student.setId(12);
obj_Student.getId();
}
catch(Exception e) {
System.out.println("Null Pointer ");
}
}
}
2 ответа
Как правило, когда вы анализируете случай в программе проверки теорем, многие случаи сводятся к «не может быть». Например, если вы доказываете некоторый факт о целых числах, вам может потребоваться выполнить анализ случая того, является ли целое число i положительным, нулевым или отрицательным. Но в вашем контексте могут быть и другие гипотезы, или, возможно, какая-то часть вашей цели, что противоречит одному из случаев. Например, вы можете знать из предыдущего утверждения, что i никогда не может быть отрицательным.
Подумайте об этом, как в компьютерной программе:
switch (k) {
case X:
/* do stuff */
break;
case Y:
/* do other stuff */
break;
default:
assert(false, "can't ever happen");
}
Цель false = true - «никогда не случится». Но вы не можете просто заявить о себе в Coq. На самом деле вы должны записать проверочный термин.
Итак, выше, вы должны доказать нелепую цель false = true. И единственное, с чем вам нужно работать - это гипотеза H: andb false c = true. Мгновенная мысль покажет вам, что на самом деле это абсурдная гипотеза (потому что andb false y сводится к ложному для любого y и, следовательно, не может быть правдой). Таким образом, вы бьете по цели, имея в своем распоряжении единственную вещь (а именно H), и ваша новая цель - false = andb false c.
Таким образом, вы применяете абсурдную гипотезу, пытаясь достичь абсурдной цели. И вот, в итоге вы получите что-то, что вы действительно сможете показать рефлексивностью. QED.
ОБНОВЛЕНИЕ Формально, вот что происходит.
Напомним, что каждое индуктивное определение в Coq имеет принцип индукции. Вот типы принципов индукции для равенства и предложение False (в отличие от термина false типа bool):
Check eq_ind.
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
: forall P : Prop, False -> P
Этот принцип индукции для False говорит, что если вы дадите мне доказательство False, я могу дать вам доказательство любого предложения P.
Принцип индукции для eq является более сложным. Давайте рассмотрим это только в bool. И конкретно к false. В нем говорится:
Check eq_ind false.
eq_ind false
: forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y
Итак, если вы начнете с некоторого предложения P(b), которое зависит от логического значения b, и у вас есть доказательство P(false), то для любого другого логического значения y, которое равно false, у вас есть доказательство P(y).
Это не звучит ужасно захватывающе, но мы можем применить его к любому предложению P, которое мы хотим. И мы хотим особенно неприятного.
Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
: (fun b : bool => if b then False else True) false ->
forall y : bool,
false = y -> (fun b : bool => if b then False else True) y
Немного упрощая, это говорит True -> forall y : bool, false = y -> (if y then False else True).
Итак, для этого требуется доказательство True, а затем некоторое логическое значение y, которое мы можем выбрать. Итак, давайте сделаем это.
Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
: false = true -> (fun b : bool => if b then False else True) true
И вот мы: false = true -> False.
В сочетании с тем, что мы знаем о принципе индукции для False, мы имеем: если вы дадите мне доказательство false = true, я могу доказать любое предложение.
Итак, вернемся к andb_true_elim1. У нас есть гипотеза H, то есть false = true. И мы хотим доказать какую-то цель. Как я показал выше, существует термин «доказательство», который превращает доказательства из false = true в доказательства того, что вы хотите. Так, в частности, H является доказательством false = true, так что теперь вы можете доказать любую цель, которую хотите.
Тактика - в основном механизм, который строит термин доказательства.
Я понимаю, что это старо, но я хочу прояснить некоторую интуицию, лежащую в основе ответа Ламбдагека (в случае, если кто-то найдет это)
Я заметил, что ключевым моментом является то, что мы определяем функцию F:bool->Prop с разными значениями в каждой точке (т. е. true => True и false => False). Однако из принципа индукции для равенства легко можно показать eq_ind интуитивную идею, что
forall A:Type, forall P:A->Prop, forall x y:A, (x=y) -> (P x = P y),
Но тогда это будет означать, что, предполагая true=false, мы имеем True=False, но поскольку мы знаем True ], мы выводим False.
Это означает, что фундаментальным свойством, которое мы используем, является способность определять F, который задается принципом рекурсии для bool, bool_rect:
forall P:bool -> Type, P true -> P false -> (forall b:bool, P b)
путем установки P (b:bool) := b=>Prop. ], то это то же самое, что и
Prop -> Prop -> (forall b:bool, Prop),
, где мы вводим True и False, чтобы получить нашу функцию F.