Ведение информации при использовании индукции?

Я использую помощник Coq Proof Assistant для реализации модели (небольшого) языка программирования (расширения реализации полулегкой Java от Bruno De Fraine, Erik Ernst, Mario Südholt). Одна вещь, которая продолжает развиваться при использовании тактики induction, заключается в том, как сохранить информацию, заключенную в конструкторы типов.

У меня есть вспомогательный ввод Prop, реализованный как

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

где extends - механизм расширения класса, как показано на Java, и typ представляет два разных типа доступных типов,

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

Примером того, где я хотел бы сохранить информацию типа, является использование тактики induction при гипотезе типа

H: sub_type (c_typ u) (c_typ v)

например. в

u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

с помощью induction H. отбрасывает всю информацию о u и v. Случай st_refl становится

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

Как вы можете видеть информацию о том, что u и v связаны с конструкторами typ в H и, следовательно, с t, теряются. Хуже всего то, что из-за этого Coq не может видеть, что u и v на самом деле должны быть одинаковыми в этом случае.

При использовании тактики inversion на H Coq удается увидеть, что u и v совпадают. Однако эта тактика здесь не применима, так как мне нужны гипотезы индукции, которые induction генерирует для доказательства случаев st_trans и st_extends.

Есть ли тактика, которая объединяет лучшие из inversion и induction, чтобы генерировать гипотезы индукции и выводить равенства без разрушения информации о том, что обернуто в конструкторах? В качестве альтернативы, есть ли способ вручную получить необходимую мне информацию? info inversion H и info induction H показывают, что множество преобразований применяется автоматически (особенно с inversion). Это привело меня к эксперименту с тактикой change наряду с конструкцией let ... in, но без какого-либо прогресса.

Ответы

Ответ 1

Это общая проблема, когда вам нужно вводить гипотезу с зависимым типом (sub_type (c_typ u) (c_typ v)), параметры которого имеют определенную структуру (c_typ u). Существует общий трюк, который заключается в выборочной перезаписи структурированного параметра в переменную, сохраняя равенство в среде.

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1.
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2.
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).

Так как Coq 8.2, этот общий шаблон set-assert-clearbody выполняется встроенной тактикой remember term as ident in *goal_occurences*.

Здесь была использована глупая лемма, использующая эту тактику.

Lemma subtype_r_left_equal :
  forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2.
Proof.
  intros.
  remember (r_typ r1) as t1 in H.
  induction H.
  congruence.
  solve [firstorder].
  discriminate.
Qed.

Бонусный наконечник (из опыта, но прошло некоторое время, поэтому я не помню деталей): когда вы делаете довольно синтаксические рассуждения о системах типов (что имеет тенденцию иметь место, когда вы делаете эти виды механических доказательств), может быть удобно продолжать печатать суждения в Set. Подумайте о наборе дериваций в качестве объектов, о которых вы рассуждаете. Я помню случаи, когда было удобно вводить равенства для типизации вывода, что не всегда работает с типированием дифференцирования в Prop.

С вашим Problem.v, здесь доказательство случая рефлексивности. Для транзитивности я подозреваю, что ваша гипотеза индукции недостаточно сильна. Это может быть побочным продуктом того, как вы упростили проблему, хотя транзитивность часто требует неожиданно задействованных гипотез или лекций индукции.

Fact sub_type_fields: forall u v fsv,
  sub_type (c_typ u) (c_typ v) -> fields v fsv ->
  exists fs, fields u (fsv ++ fs).
Proof.
  intros.
  remember (c_typ u) as t1 in H.
  remember (c_typ v) as t2 in H.
  induction H.
  (* case st_refl *)
  assert (v = u). congruence. subst v t.
  exists nil. rewrite <- app_nil_end. assumption.
  (* case st_trans *)
  subst t1 t3.
  (* case st_extends *)
Admitted.

Ответ 2

Я столкнулся с подобной проблемой, и тактика Coq 8.3 "зависимая индукция" позаботилась о бизнесе.

Ответ 3

Я был уверен, что у CPDT есть некоторые комментарии по этой проблеме, но это не совсем очевидно, где это. Вот несколько ссылок:

http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html Раздел "Предикаты с неявным равенством" показывает, возможно, самый простой случай, когда Coq "теряет информацию" (на destruct, а не индукция.) Это также объясняет, почему эта информация теряется: когда вы уничтожаете тип, применяемый к аргументу, который не является свободной переменной, эти типы сначала заменяются на свободные переменные (поэтому Coq теряет информацию. )
http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html В разделе "Способы избежания аксиом" показаны некоторые трюки для избежания аксиомы K, включая описанный "трюк равенства" Жилем. Найдите "использование общего трюка на основе равенства для поддержки индукции по аргументам без переменной для типов семейств"

Я думаю, что это явление тесно связано с зависимым сопоставлением шаблонов.