In lotta con la tattica della riscrittura in Idris

Question

Sto esaminando il vero libro di analisi di Terry Tao, che costruisce la matematica fondamentale dai numeri naturali in su. Formulando quante più prove possibili, spero di familiarizzare con Idris e tipi dipendenti.

Ho definito il seguente tipo di dati:

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

rappresentare la proposizione che un numero naturale è maggiore o uguale a un altro.

Attualmente sto lottando per dimostrare riflessività di questo rapporto, vale a dire di costruire la prova con la firma

geRefl : GE n n 

Il mio primo tentativo è stato quello di provare semplicemente geRefl {n} = Ge n Z, ma questo ha digitare Ge n (add n Z). Per ottenere questo di unificare con la firma desiderata, dobbiamo ovviamente di effettuare una sorta di riscrittura, presumibilmente coinvolge il lemma

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

mio miglior tentativo è la seguente:

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

ma questo non TYPECHECK .

Potete per favore fornire una dimostrazione corretta di questo teorema e spiegare il ragionamento alla base di questo teorema?

Answer 1

Il primo problema è superficiale: si sta tentando di applicare la riscrittura nel posto sbagliato. Se si dispone di x : GE n (n + Z), allora si dovrà riscrivere il suo tipo, se si desidera utilizzare come la definizione di geRefl : GE n n, in modo che ci si dovrà scrivere

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

ma che ancora non funziona. Il vero problema è che si desidera solo riscrivere una parte del tipo GE n n: se la si riscrive semplicemente usando n + 0 = n, si ottiene GE (n + 0) (n + 0), che non è ancora possibile provare usando Ge n 0 : GE n (n + 0).

Quello che dovete fare è usare il fatto che se a = b, quindi x : GE n a può essere trasformato in x' : GE n b. Questo è esattamente ciò che la funzione replace nella libreria standard fornisce:

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

Usando questo, impostando P = GE n, e l'utilizzo di Ge n 0 : GE n (n + 0), possiamo scrivere geRefl come

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

(notare che Idris è perfettamente in grado per dedurre il parametro implicito P, quindi funziona senza, ma in questo caso penso che chiarisca cosa sta succedendo)