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

Это общая проблема, когда вам нужно провести индукцию по гипотезе с зависимым типом (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.

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

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

1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html В разделе «Предикаты с неявным равенством» показан, пожалуй, самый простой случай, когда Coq «теряет информацию» (при разрушении, а не индукции). Он также объясняет, ПОЧЕМУ эта информация теряется: когда вы разрушаете тип, применяемый к аргумент, который не является свободной переменной, эти типы сначала заменяются свободными переменными (вот почему Coq теряет информацию).

2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html В разделе «Методы ухода от аксиом» показаны некоторые уловки, позволяющие избежать аксиомы K, в том числе «уловка равенства», описанная Жилем. Найдите «использование общего трюка, основанного на равенстве, для поддержки индукции по неизменяемым аргументам для семейств типов»

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