Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade
Last active November 3, 2022 21:03
Show Gist options
  • Save Blaisorblade/0b312c4e76d01538f783b372052c876a to your computer and use it in GitHub Desktop.
Save Blaisorblade/0b312c4e76d01538f783b372052c876a to your computer and use it in GitHub Desktop.
Coq unification is up to convertibility but does not compute normal forms
Require Import ssreflect.
Fixpoint ackn (m : nat) (ack : nat -> nat) {struct m} :=
match m with
| O => ack 1
| S q => ack (ackn q ack)
end.
Fixpoint ack (n m : nat) {struct n} : nat :=
match n with
| O => S m
| S p => ackn m (ack p)
end.
Lemma ack_S m n : ack (S m) n = ackn n (ack m).
Proof. reflexivity. Qed.
Fail Timeout 1 Eval compute in ack 4 4.
Fail Timeout 1 Eval vm_compute in ack 4 4.
Goal ack 4 4 = ack 4 4.
reflexivity.
Restart.
rewrite {1}ack_S.
Fail Timeout 1 reflexivity.
Abort.
Goal ack (3 + 1) 4 = ack 4 4.
reflexivity.
Goal ack 3 4 = ack 4 4.
Timeout 1 reflexivity.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment