Versuchen Konzept der indizierte Art Familie

Question

Mit der folgenden Definition zu verstehen:

Inductive eq (A : Type) (x : A) : A → Prop := eq refl : (eq x) x 

Parameter a b : A. 

Wenn ich bedenke, eines seiner Instanz eq a b, las ich (eq a) vom Typ A -> Prop.

Dann ist meine Frage, dass wie (eq a) b die Tatsache feststellen kann, dass a und b dem gleichen Objekt entspricht?

Das Merkwürdige an mir ist, dass wir keine Informationen darüber haben, was (eq a) tatsächlich tun.

Answer 1

Eq a ist ein Prädikat, das nur definiert ist (hat nur den Einwohner eq_refl), wenn sein Argument gleich b ist, wobei Gleichheit "bis zur Vereinheitlichung durch den Typchecker" bedeutet. So muss a von Coq gesehen werden, um dasselbe wie b zu sein, andernfalls ist Äq a b äquivalent zu Falsch.

Answer 2

zu Johns Antwort hinzuzufügen, scheinen die Menschen die informelle Beschreibung zu schätzen Ich habe hier, wie ich denke, intuitiv indizierter Typ Familien:

https://stackoverflow.com/a/24601292/553003

würde ich noch hinzufügen, dass es einen Unterschied zwischen der ist Geben Sie (eq a) b (das ist das gleiche wie eq a b) und einen Begriff, der diesen Typ hat.

Zum Beispiel können Sie festlegen:

Definition a_weird_type : Type := eq 0 42. 

Da eine solche Art ohne Beweis nur eine Aussage. Sie sollten a_weird_term mit dem Typ a_weird_type jedoch nicht definieren können, da Sie das System niemals davon überzeugen werden, dass 0 und 42 tatsächlich gleich sind.

Beachten Sie, dass es zwar noch ein wenig Kontrolle, so dass Sie nicht definieren:

Definition a_weirder_type : Type := eq 42 true. (* Coq will reject this *) 

Da der eq Typ den Typ der Elemente implizit trägt sie, und das Typsystem wird sichergestellt, dass die vergleicht zwei Elemente haben diesen Typ:

Check (@eq nat 42 true). 
(*    ^^^^ this should have type nat *) 

Check (@eq bool 42 true). 
(*    ^^ this should have type bool *) 

Check (@eq nat 23 42). 
(* fine, but not provable *)