Kämpfen mit Rewrite-Taktik in Idris

Question

Ich gehe durch Terry Taos echtes Analyse-Lehrbuch, das grundlegende Mathematik von den natürlichen Zahlen aufbaut. Indem ich so viele Beweise wie möglich formalisiere, hoffe ich, mich sowohl mit Idris als auch mit abhängigen Typen vertraut zu machen.

I haben die folgenden Datentypen definiert:

data GE: Nat -> Nat -> Type where 
    Ge : (n: Nat) -> (m: Nat) -> GE n (n + m) 

den Satz zu repräsentieren, dass eine natürliche Zahl größer als oder gleich zu einem anderen.

Ich kämpfe derzeit Reflexivität dieser Beziehung zu beweisen, das heißt den Beweis mit Unterschrift war

geRefl : GE n n 

Mein erster Versuch zu konstruieren einfach geRefl {n} = Ge n Z versuchen, aber das hat Ge n (add n Z) geben. Um dies mit der gewünschten Signatur zu vereinen, müssen wir offensichtlich eine Art von Umschreiben auszuführen, vermutlich unter Beteiligung der Lemma

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left 

Mein bester Versuch ist die folgende:

geRefl : GE n n                 
geRefl {n} = x                 
    where x : GE n (n + Z)              
      x = rewrite plusZeroRightNeutral n in Ge n Z 

aber dies nicht typecheck .

Können Sie bitte einen korrekten Beweis für dieses Theorem geben und die Gründe dafür erklären?

Answer 1

Das erste Problem ist oberflächlich: Sie versuchen, das Umschreiben an der falschen Stelle anzuwenden. Wenn Sie x : GE n (n + Z) haben, dann werden Sie seine Art neu zu schreiben, wenn Sie es wie die Definition von geRefl : GE n n verwenden möchten, so würden Sie

geRefl : GE n n 
geRefl {n} = rewrite plusZeroRightNeutral n in x 

Aber das wird immer noch funktionieren nicht schreiben. Das eigentliche Problem ist, dass Sie nur einen Teil des Typs GE n n neu schreiben wollen: Wenn Sie es nur mit n + 0 = n umschreiben, erhalten Sie GE (n + 0) (n + 0), die Sie immer noch nicht mit Ge n 0 : GE n (n + 0) beweisen können.

Was Sie tun müssen, ist die Tatsache nutzen, dass, wenn a = b, dann x : GE n a in x' : GE n b gedreht werden kann. Das ist genau das, was die replace Funktion in der Standardbibliothek bietet:

replace : (x = y) -> P x -> P y 

diese mithilfe von P = GE n Einstellungen und Verwendung Ge n 0 : GE n (n + 0) können wir geRefl als

geRefl {n} = replace {P = GE n} (plusZeroRightNeutral n) (Ge n 0) 

schreiben (beachten Sie, dass Idris durchaus in der Lage ist den impliziten Parameter P abzuleiten, so funktioniert es ohne, aber ich denke in diesem Fall macht es klarer, was passiert)