Coq Inferenz Verhalten

Question

Ich versuche, das folgende Agda-Snippet in Coq zu schreiben.

open import Data.Fin using (Fin; suc; zero) 
open import Data.Nat using (ℕ; suc; zero) 

thin : {n : ℕ} -> Fin (suc n) -> Fin n -> Fin (suc n) 
thin zero y  = suc y 
thin (suc x) zero = zero 
thin (suc x) (suc y) = suc (thin x y) 

Ich dachte, das ohne weiteres zu Coq übersetzt werden könnte wie:

Inductive Fin : nat -> Type := 
    | fz {n : nat} : Fin (S n) 
    | fs {n : nat} : Fin n -> Fin (S n). 

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) := 
    match x, y with 
    | fz,  y' => fs y' 
    | (fs x'), fz => fz 
    | (fs x'), (fs y') => fs (thin x' y') 
    end. 

Dies führt jedoch zu dem folgenden Fehler:

Toplevel input, characters 171-173: 
Error: 
In environment 
thin : forall n : nat, Fin (S n) -> Fin n -> Fin (S n) 
n : nat 
x : Fin (S n) 
y : Fin n 
n0 : nat 
x' : Fin n0 
n1 : nat 
y' : Fin n1 
The term "x'" has type "Fin n0" while it is expected to have type 
"Fin (S ?n1)". 

Ich glaube, Coq Figur Lage sein sollte, out den impliziten Parameter n so habe ich keine Ahnung, was vor sich geht. Ich denke, mir ist ein Unterschied zwischen den Typsystemen von Agda und Coq nicht bewusst, da die früheren Typchecks gut waren.

Answer 1

Bei der Mustererkennung mit abhängigen Typen berücksichtigt Coq normalerweise nicht einige wesentliche Beziehungen zwischen den Variablen im Kontext und den in den Verzweigungen eingeführten Variablen.

Die einfachste Lösung ist, die Funktion im Proof-Modus zu definieren, zumindest um zu verstehen, was vor sich geht.

Dies gibt:

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n). 
Proof. 
    remember (S n) as n1. (* trick to keep the information when destructing *) 
    destruct x; apply eq_add_S in Heqn1; subst n0. 
    - apply fs. assumption. 
    - destruct y. 
    + apply fz. 
    + apply fs. apply thin; assumption. 
Defined. (* to create a transparent constant, as given by a classic Fixpoint *) 

Sie dann den Wert drucken können, und die Lambda-Begriff zu verstehen, wie Sie es direkt zu definieren. Dies könnte geben:

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) := 
    match x as x0 in Fin k return k = S n -> Fin (S n) with 
    | fz => fun _ => fs y 
    | fs x' => 
     fun H => match y as y0 in Fin l return n = l -> Fin (S n) with 
     | fz => fun _ => fz 
     | fs y' => fun H' => 
      fs (eq_rec_r (fun x => Fin x) 
         (thin (eq_rec_r _ 
           (eq_rec_r _ x' (eq_add_S _ _ (eq_sym H))) 
           (eq_sym H')) 
           y') 
         H') 
     end eq_refl 
    end eq_refl. 

Die return Klauseln der Muster Matchings verwendet wird, um das Problem, das oben dargestellt zu lösen: sie die Variablen eingeführt in den Zweigen und die, die im Rahmen verbinden. Dies wird hier genauer diskutiert: http://adam.chlipala.net/cpdt/html/MoreDep.html.

Beachten Sie auch, dass dieser spezielle induktive Typ vor ein paar Wochen auf der coq-club Mailingliste diskutiert wurde. Siehe https://sympa.inria.fr/sympa/arc/coq-club/2016-03/msg00206.html.

Answer 2

Wenn Sie sich an eine Syntax halten möchten, die der von Agda sehr ähnlich ist, können Sie das equations-Plugin von Sozeau verwenden. Sie können schreiben:

Require Import Equations. 

Inductive Fin : nat -> Type := 
    | fz {n : nat} : Fin (S n) 
    | fs {n : nat} : Fin n -> Fin (S n). 

Lemma FinO_elim : Fin O -> False. 
Proof. 
inversion 1. 
Qed. 

Equations thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) 
:= thin {n:=O}  _  y  :=! y (* y is uninhabited *) 
; thin fz  y  := fs y 
; thin (fs x) fz  := fz 
; thin (fs x) (fs y) := fs (thin x y) 
. 

You can also remove the first dead-code clause which is automatically inferred.