DPM-NBE

Experiments on implementing Dependent Pattern Matching under Normalization by Evaluation setup.

Syntax

Example

let trans : (A : U) (a b c : A) -> Id A a b -> Id A b c -> Id A a c =
  λ A a b c refl refl . refl; 

let cong : (A B : U) (f : A -> B) (a b : A) -> Id A a b -> Id B (f a) (f b) =
  λ A B f a b refl . refl;

let H : (m n : Nat) -> Id Nat n (plus m zero) -> Id Nat m zero -> Id Nat n zero =
  λ m n refl refl . refl;

let C : (A : U) -> Id Nat (suc zero) zero -> A = 
  λ A (!); -- Absurd pattern

U

Note.

• plus, suc, Id must be fully applied.

• For simplicity, we only have refl , absurd pattern (!) and variables as patterns, zero and suc are not patterns.

  The idea is to isolate DEPENDENT part from dependent pattern matching.

Difficulty of DPM under NbE

The problem is that a value is not stable under substitution, for example, when we checking the following pattern matching

let H : (m n : Nat) -> Id Nat n (plus m zero) -> Id Nat m zero -> ... 
  λ m n refl refl . ...  

For the first refl, we need to unify n with plus m zero, extending the evaluation environment with n = plus m zero, which is a value (corresponding to a normal form). But the second refl gives m = zero, which makes the plus m zero [zero/m] no more a normal form.

Acknowledgements

• The base code is directly copied from András Kovács' elaboration zoo.

• The idea of the solution to DPM under NbE problem is also directly from Kovács' cctt and his talk, using explicit substitutions and forcing.

• The unification algorithm for solving the unification problems generated by DPM is from Ulf Norell's thesis and Jesper Cockx Dominique Devriese Frank Piessens' Pattern Matching Without K. Note that I do "with-K" here, but it is not a problem to change to "without-K".