Удаление tcast из кортежей ... Сезон 2 - PullRequest
Новая
       82

Удаление tcast из кортежей ... Сезон 2

0 голосов
/ 09 мая 2020

Я бы хотел удалить tcast в «лемме», например, в следующей. Но это даже не проверка типов из-за «ограничений» зависимой типизации. 

Lemma foo : forall {T} m n (tc : n = m) (f : m.-tuple T -> 'I_n -> nat) (x : n.-tuple T),
    [seq f (tcast tc x) j | j <- enum 'I_n] =  
    [seq f x j | j <- enum 'I_n].

Фактически, более важным примером для приложения, которое я имею в виду и которое выполняет проверку типов, была бы следующая лемма: 

Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i = 
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.

Это было бы просто на seq, но здесь я не могу найти, как продолжить использование лемм в tuple.v или fintype.v.

Итак, как правильно обращаться с такими tcast выражениями, когда они кажутся неподходящими на лечение через val_inj и анализ случая (см. предыдущий пост)? Должен ли я в первом примере представить две версии f, которые позже оказались равными по последовательностям (и если да, то как лучше всего продолжить)?

Заранее спасибо за любое предложение.

Пьер

1 Ответ

0 голосов
/ 13 мая 2020

В случае, если вы публикуете, вы можете удалить приведение, используя стандартный прием: 

Lemma val_tcast {T} m n (tc : n = m) (x : n.-tuple T) :
  val (tcast tc x) = val x.
Proof. by case: m / tc. Qed.

Lemma sum_tuple n (t : n.-tuple nat) :
 \sum_(i < n) tnth t i = \sum_(i < n) nth 0 (val t) i.
Proof. by apply: eq_bigr => ? ?; rewrite (tnth_nth 0). Qed.

Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof.
rewrite !sum_tuple val_tcast /=.

Tho есть прямое доказательство: 

Lemma bar' n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof. by rewrite -!(big_tuple _ _ _ predT id) val_tcast big_cat. Qed.
...