Geek Answers Handbook

Why sometimes I can prove the goal through a lemma, but not directly?

Consider the function defined below. It is not very important what he does.

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.

I want to prove

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

After doing

  simpl. unfold eq_rect_r. unfold eq_rect.

purpose

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

When trying to complete it with

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

destructnot working (see error message below). However, if I first prove the exact same goal in the lemma or even with the assertinside of the proof, I can apply and solve it, for example:

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.

Can someone explain why this is so, and how to think about this situation when he is faced with it?

In Coq 8.4, I get an error

      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.

and in Coq 8.5 I get an error

      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".
+4
source share
2 answers

- , ( Set Printing All. ).

, , , , , ( , ). , , .

+1

@ 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. . 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.

: coq-.

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.
+2

More articles:


All Articles