Абстрагирование приводит к некорректно набранному, но хорошо напечатанному термину

На какое-то время я застрял в проблеме, для которой я привел небольшой автономный пример:

Axiom f : nat -> Set.

Goal forall (n : nat) (e : n = n) (x : f n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

Теперь, если вы попытаетесь destruct e, вы получите следующее сообщение об ошибке:

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : n0 = n0) =>
 forall x : f n0,
 match e in (_ = _n) return (f _n -> Prop) with
 | Logic.eq_refl => fun v : f n0 => v = x
 end x" which is ill-typed.

Некоторое время почесав затылок, я не мог понять, что в этом термине было неправильно набрано ... Итак, я попробовал это:

Definition illt :=
  fun (n : nat) (e : n = n) =>
  forall x : f n,
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

И Coq принимает это, набирая forall n : nat, n = n -> Prop.

Итак, что не так с этим сообщением об ошибке, и как я могу решить / настроить свою первоначальную цель?

Кстати, это все coq8.3. Если что-то исправлено в 8.4, пожалуйста, сообщите мне и приношу свои извинения! :)

РЕДАКТИРОВАТЬ: Чтобы обратиться к комментарию Робина Грина, вот Set Printing All версии сообщения об ошибке:

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : @eq nat n0 n0) =>
 forall x : f n0,
 match e in (@eq _ _ _n) return (f _n -> Prop) with
 | eq_refl => fun v : f n0 => @eq (f n0) v x
 end x" which is ill-typed.

Это хорошо набранный термин, и ничего не подразумевается.


coq
person Ptival    schedule 14.02.2013    source источник
comment
Если вы включите отображение всех скрытых аспектов, вы можете найти то, что написано неправильно. К сожалению, по умолчанию Coq не всегда дает вам полный термин, о котором он думает, в сообщениях об ошибках. Попробуйте Set Printing All.   -  person Robin Green    schedule 15.02.2013
comment
@RobinGreen Конечно, это хорошо в целом, но здесь единственный подразумеваемый параметр - это первый параметр eq, и это, похоже, вообще не приводит к нетипизированности ...   -  person Ptival    schedule 15.02.2013
comment
На самом деле eq имеет три параметра (первый - это тип), а первые два здесь неявны.   -  person Robin Green    schedule 15.02.2013
comment
В (e : n = n) nat неявно, но выводимо. В _ = _n два параметра типа не должны указываться, должны быть названы только индексы. В v = x f n неявно, но выводимо. Я не думаю, что здесь есть проблема с имплицитами.   -  person Ptival    schedule 15.02.2013

Ответы (1)


arrow_upward
3
arrow_downward

Вот возможное объяснение проблемы. То, что происходит при построении конструкции сопоставления с образцом, также можно описать с помощью теоремы. Вот мой взгляд на теорему, которая используется в вашем случае.

Check eq_rect.

eq_rect
 : forall (A : Type) (x : A) (P : A -> Type),
   P x -> forall y : A, x = y -> P y

Поэтому при сопоставлении с образцом на равенстве вы должны предоставить формулу P, параметризованную на любом значении y, которое оказывается доказуемо равным x. Интуитивно вы должны иметь возможность заменить свое выражение сопоставления с образцом на apply eq_rect, но свойство P, которое должно появиться там, находится за пределами досягаемости того, что Coq может угадать, потому что каждое вхождение x в вашей формуле обязательно относится к типу f n и не может быть просто типа f m где m = n. В сообщении об ошибке не говорится об этом, возможно, это ошибка.

Чтобы выполнить ваше доказательство, я предлагаю скорее использовать тот факт, что доказательства равенства уникальны в определенных классах типов, и nat принадлежит к такому классу. Это лечится в файле Eqdep_dec.

Require Eqdep_dec Arith.

Теперь ваше доказательство проходит довольно легко.

Goal forall n (x : f n) (e : n = n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.
intros n x e; replace e with (eq_refl n).
  reflexivity.
apply Eqdep_dec.UIP_dec, eq_nat_dec.
Qed.

Теперь это решение может показаться неудовлетворительным. Откуда это UIP_dec? UIP означает уникальность подтверждения личности, и, к сожалению, это свойство не гарантируется для всех произвольных типов. Это гарантировано для всех типов, где равенство разрешимо (как выражено UIP_dec), например nat.

person Yves    schedule 18.02.2013
comment
Спасибо за очень подробный ответ. Я, наконец, отказался от SO и разместил сообщение в Coq Club, вы, возможно, видели это, и вот ветка: sympa.inria.fr/sympa/arc/coq-club/2013-02/msg00041.html Итак, чтобы доказать, что все доказательства рефлексивности являются eq_refl, я использовал UIP, доказанный в случае разрешимых типов: в моем фактическом примере не было nat, как здесь, а был тип desc или описания, где f было обозначением этого описания к фактическому типу, который он обозначает. Тем не менее, ваш ответ очень интересен! И HTT тоже, хотя на данный момент мне это совершенно не по зубам! :) - person Ptival; 18.02.2013