Почему я могу иногда доказывать цель через лемм, но не напрямую?

Question

Рассмотрим функцию, определенную ниже. Не важно, что он делает.

Require Import Ring. 
Require Import Vector. 
Require Import ArithRing. 

Fixpoint 
    ScatHUnion_0 {A} (n:nat) (pad:nat) : t A n -> t (option A) ((S pad) * n). 
refine (
    match n return (t A n) -> (t (option A) ((S pad)*n)) with 
    | 0 => fun _ => (fun H => _)(@nil (option A)) 
    | S p => 
    fun a => 
     let foo := (@ScatHUnion_0 A p pad (tl a)) in 
     (fun H => _) (cons _ (Some (hd a)) _ (append (const None pad) foo)) 
    end 
    ). 
rewrite <-(mult_n_O (S pad)); auto. 
replace (S pad * S p) with ((S (pad + S pad * p))); auto; ring. 
Defined. 

Я хочу доказать

Lemma test0: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)). 

После выполнения

simpl. unfold eq_rect_r. unfold eq_rect. 

цель

  match mult_n_O 1 in (_ = y) return (t (option nat) y) with 
     | eq_refl => nil (option nat) 
     end = nil (option nat) 

При попытке закончить его с

apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto. 
    destruct (mult_n_O 1); auto. 

destruct не работает (см. Ниже для сообщения об ошибке). Однако, если я сначала доказать, точно такие же цели в лемме или даже с assert внутри доказательства, я могу применить и решить, как это:

Lemma test1: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)). 
    simpl. unfold eq_rect_r. unfold eq_rect. 

    assert (
     match mult_n_O 1 in (_ = y) return (t (option nat) y) with 
     | eq_refl => nil (option nat) 
     end = nil (option nat) 
    ) as H. 
    { 
    apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto. 
    destruct (mult_n_O 1); auto. 
    } 
    apply H. 
Qed. 

Может кто-нибудь объяснить, почему это, и как следует подумать об этой ситуации, когда кто-то сталкивается с этим?

---

В Coq 8.4 Я получаю ошибку

 Toplevel input, characters 0-21: 
     Error: Abstracting over the terms "n" and "e" leads to a term 
     "fun (n : nat) (e : 0 = n) => 
     match e in (_ = y) return (t (option nat) y) with 
     | eq_refl => nil (option nat) 
     end = const None n" which is ill-typed. 

и в Coq 8.5 Я получаю ошибку

 Error: Abstracting over the terms "n" and "e" leads to a term 
     fun (n0 : nat) (e0 : 0 = n0) => 
     match e0 in (_ = y) return (t (option nat) y) with 
     | eq_refl => nil (option nat) 
     end = const None n0 
     which is ill-typed. 
     Reason is: Illegal application: 
     The term "@eq" of type "forall A : Type, A -> A -> Prop" 
     cannot be applied to the terms 
     "t (option nat) 0" : "Set" 
     "match e0 in (_ = y) return (t (option nat) y) with 
     | eq_refl => nil (option nat) 
     end" : "t (option nat) n0" 
     "const None n0" : "t (option nat) n0" 
     The 2nd term has type "t (option nat) n0" which should be coercible to 
     "t (option nat) 0". 

Answer 1

Я бы сказал, что это из-за зависимых типов, и вы не фактически доказывают то же самое в обоих случаях (попробуйте Set Printing All., чтобы увидеть неявные типы и скрытую информацию).

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

Answer 2

@ Vinz ответ объяснил причину, и предложил Set Printing All., который показывает, в чем разница. Проблема заключалась в том, что simpl. упростил тип возврата match. Использование unfold ScatHUnion_0. вместо simpl. позволило мне использовать разрушение непосредственно на цели.

В сущности, мои проблемы возникли из-за меня, чтобы убедить систему типов, что 0=0 - это то же самое, что и 0=1*0. (Кстати, я до сих пор не знаю, как это сделать.) Я использовал mult_n_O, чтобы показать это, но он непрозрачен, поэтому система типов не могла развернуть его, проверяя, что эти два типа были равны.

Когда я заменил его с моим собственным Fixpoint вариант (который не является непрозрачной),

Fixpoint mult_n_O n: 0 = n*0 := 
    match n as n0 return (0 = n0 * 0) with 
    | 0 => eq_refl 
    | S n' => mult_n_O n' 
    end. 

и использовать его в определении ScatHUnion_0, лемма была тривиальной, чтобы доказать:

Lemma test0: @ScatHUnion_0 nat 0 0 (@nil nat) = (@nil (option nat)). 
    reflexivity. 
Qed. 

---

Дополнительный комментарий:

Вот доказательство того, что работает с оригинальным непрозрачным определением mult_n_O. Он основан на proof by Jason Gross. Он управляет типом mult_n_O 1 как 0=0, используя generalize. Он использует set для изменения неявных частей термина, например типа eq_refl, который отображается только после команды Set Printing All.. change также может это сделать, но replace и rewrite, похоже, не в состоянии это сделать.

Lemma test02: 
    match mult_n_O 1 in (_ = y) return (t (option nat) y) with 
    | eq_refl => nil (option nat) 
    end = nil (option nat). 
Proof. 
    Set Printing All. 
    generalize (mult_n_O 1 : 0=0). 
    simpl. 
    set (z:=0) at 2 3. 
    change (nil (option nat)) with (const (@None nat) z) at 2. 
    destruct e. 
    reflexivity. 
Qed. 

---

Update: Вот еще проще доказательство благодаря людям в Кок-клубе.

Lemma test03: 
    match mult_n_O 1 in (_ = y) return (t (option nat) y) with 
    | eq_refl => nil (option nat) 
    end = nil (option nat). 
Proof. 
    replace (mult_n_O 1) with (@eq_refl nat 0); 
    auto using Peano_dec.UIP_nat. 
Qed.