MPRI PRFA 2025 Test file

Go back to the course page.

This test file should run perfectly if you have Rocq 9.0 installed as well as the required Equations and MetaCoq version.

You only need to make sure you can interpret the whole file, not understand it.

(* This should test that you have Rocq installed *)
From Stdlib Require Import Lia.

(* This should test that you also have Equations *)
From Equations Require Import Equations.

(* And MetaRocq Template *)
From MetaRocq.Template Require Import All.

(* Testing Equations *)
Equations eq_test (x : bool) : nat :=
  eq_test true := 12 ;
  eq_test false := 1.
eq_test is defined
eq_test is defined
eq_test_equation_1 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_equation_1 is defined
eq_test_equation_2 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_equation_2 is defined
eq_test_graph is defined
eq_test_graph_rect is defined
eq_test_graph_rect is recursively defined
eq_test_graph_correct has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_graph_correct is defined
eq_test_elim has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_elim is defined
FunctionalElimination_eq_test is defined
FunctionalInduction_eq_test is defined

(* Testing MetaRocq *)
MetaRocq Quote Definition eq_test_term := eq_test.
eq_test_term is defined
Print eq_test_term.
eq_test_term = tConst (MPfile ["test_file"%bs]%list, "eq_test"%bs) []%list
     : term