Beweisen Sie, dass die einzige Null-Längen-Vektor ist gleich Null

Question

ich ein Typ wie

Inductive bits : nat -> Set := 
| bitsNil : bits 0 
| bitsCons : forall {l}, bool -> bits l -> bits (S l). 

definiert haben und ich versuche zu beweisen:

Lemma emptyIsAlwaysNil : forall {a: bits 0}, a = bitsNil. 

Nach intros, ich habe constructor 1 versucht, case a, intuition, vergeblich. case a scheint, wie die am nächsten, aber es wird eine Fehlermeldung:

Abstracting over the terms "0" and "a" leads to a term 
fun (n : nat) (a0 : bits n) => a0 = bitsNil 
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 
"bits n" : "Set" 
"a0" : "bits n" 
"bitsNil" : "bits 0" 
The 3rd term has type "bits 0" which should be coercible to 
"bits n". 

Es klingt wie es nicht, ob ein Bit-Vektor einer beliebigen Länge, die gleich ist zu einem von der Länge Null bestimmen kann, weil sie anders sind auf der Typenebene. Ist das korrekt?

Answer 1

Ja, sind Sie grundsätzlich richtig: speziell, welche Art nicht Prüfung ist Versuch Coq eine match auf a:bits 0 zu bauen (was case tut): Der bitsCons Fall hat eine schlecht getippt Abschluss.

Hier ist ein Axiom-freier Beweis. Der Schlüsselgedanke ist, die Aussage manuell auf irgendeine n = 0 zu verallgemeinern (ich konnte nicht herausfinden, wie man das mit Taktiken macht; alle stolpern über die Abhängigkeit). Der Gleichheitsbeweis macht dann die Überprüfung der Abschlussart unabhängig davon, was n ist, und wir können den bitsCons Fall ablehnen, weil wir n = S n' haben werden. In dem schwierigeren bitsNil Fall verwenden wir eq_rect_eq_dec, was eine Konsequenz von Axiom K ist, aber beweisbar ist, wenn der Typindex (, in diesem Fall) eine entscheidbare Gleichheit hat. Siehe die Coq standard library documentation für einige andere Dinge, die Sie ohne Axiome mit entscheidbarer Gleichheit tun können.

Require PeanoNat. 
Require Import Eqdep_dec. 
Import EqNotations. 

Inductive bits : nat -> Set := 
| bitsNil : bits 0 
| bitsCons : forall {l}, bool -> bits l -> bits (S l). 

Lemma emptyIsAlwaysNil_general : 
    forall n (H: n = 0) {a: bits n}, 
    rew [bits] H in a = bitsNil. 
Proof. 
    intros. 
    induction a; simpl. 
    (* bitsNil *) 
    rewrite <- eq_rect_eq_dec; auto. 
    apply PeanoNat.Nat.eq_dec. 
    (* bitsCons - derive a contradiction *) 
    exfalso; discriminate H. 
Qed. 

Lemma emptyIsAlwaysNil : forall {a: bits 0}, 
    a = bitsNil. 
Proof. 
    intros. 
    change a with (rew [bits] eq_refl in a). 
    apply emptyIsAlwaysNil_general. 
Qed. 

Sie brauchen nicht die rew H in x Notation von EqNotations (es die Gleichheit Rekursion Prinzip nur hüllt eq_rect,), aber ich finde es Dinge viel besser lesbar macht.

Allerdings können Sie diesen Satz mehr beweisen nur, wenn Sie bereit sind, ein Axiom zu verwenden, insbesondere JMeq_eq (CPDT's equality chapter für weitere Details sehen), da dann können Sie dependent induction oder dependent destruction verwenden:

Require Import Program.Equality. 

Inductive bits : nat -> Set := 
| bitsNil : bits 0 
| bitsCons : forall {l}, bool -> bits l -> bits (S l). 

Lemma emptyIsAlwaysNil : 
    forall {a: bits 0}, a = bitsNil. 
Proof. 
    intros. 
    dependent destruction a; reflexivity. 
Qed. 

Print Assumptions emptyIsAlwaysNil. 
(* Axioms: 
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y *) 

Answer 2

Hier ist ein einfacher Beweis (von this Coq Club thread geliehen):

Definition emptyIsAlwaysNil {a: bits 0} : a = bitsNil := 
    match a with bitsNil => eq_refl end. 

Opaque emptyIsAlwaysNil. 

Hier ist das, was Coq unter der Haube baut:

Print emptyIsAlwaysNil. 

emptyIsAlwaysNil = 
fun a : bits 0 => 
match 
    a as a0 in (bits n) 
    return 
    (match n as x return (bits x -> Type) with 
    | 0 => fun a1 : bits 0 => a1 = bitsNil 
    | S n0 => fun _ : bits (S n0) => IDProp 
    end a0) 
with 
| bitsNil => eq_refl 
| bitsCons _ _ => idProp 
end 
    : forall a : bits 0, a = bitsNil