Skip to content

Commit 94e92fc

Browse files
yforsteryforster
committed
Files for POPL 24 tutorial
1 parent 0765005 commit 94e92fc

5 files changed

Lines changed: 313 additions & 0 deletions

File tree

‎popl24/MetaCoqPrelude.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
exercises/MetaCoqPrelude.v

‎popl24/exercises/MetaCoqPrelude.v‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
(* You can ignore the content of this file.
2+
3+
It provides useful notations and combinators to use in the exercises, but it is not necessary to understand their definition. *)
4+
5+
From MetaCoq.Template Require Import All Checker Reduction.
6+
7+
Notation "'$quote' x" := ltac:((let p y := exact y in
8+
quote_term
9+
x
10+
p)) (at level 0).
11+
12+
Notation "'$run' f" := ltac:(let p y := exact y in
13+
run_template_program
14+
f
15+
p) (at level 0).
16+
17+
Notation "'$quote_rec' x" := ($run (tmQuoteRec x)) (at level 0).
18+
19+
Notation "'$unquote' x" := ltac:((let p y := match y with
20+
existT_typed_term ?T ?b => exact b
21+
end in
22+
run_template_program
23+
(tmUnquote x)
24+
p)) (at level 0).
25+
26+
Notation "'$unquote' x : T" := ($run (tmUnquoteTyped T x)) (at level 0, T at level 100, x at next level).
27+
28+
Definition unfold_toplevel {A} (x : A) :=
29+
tmBind (tmQuote x) (fun y =>
30+
match y with
31+
| tConst na _ =>
32+
tmEval (unfold na) x
33+
| y => tmReturn x
34+
end).
35+
36+
Notation "'$Quote' x" := ($run (tmBind (unfold_toplevel x) (tmQuote))) (at level 0).
37+
38+
Definition term_eqb (t1 t2 : term) :=
39+
@eq_term config.default_checker_flags init_graph t1 t2.
40+
41+
Notation "t == u" := (term_eqb t u) (at level 70).
42+
43+
Open Scope bs.
44+
Open Scope bool.
45+
Open Scope list.
46+
47+
Definition tLam x A b :=
48+
tLambda {| binder_name := nNamed x; binder_relevance := Relevant |} A b.
49+
50+
Definition tLet x A t b :=
51+
tLetIn {| binder_name := nNamed x; binder_relevance := Relevant |} t A b.
52+
53+
Require Import Nat.
54+
55+
Notation "'__'" := (hole) (no associativity, at level 0).
56+

‎popl24/exercises/_CoqProject‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
-Q . ""
2+
3+
MetaCoqPrelude.v
4+
exercises.v

‎popl24/exercises/exercises.v‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
(** * MetaCoq *)
2+
3+
(** ** Print Assumptions
4+
5+
A recent question on coq-club asked
6+
7+
"Is there a way to get Print Assumptions to output fully qualified names of all items?"
8+
9+
(https://sympa.inria.fr/sympa/arc/coq-club/2024-01/msg00007.html)
10+
11+
There is no satisfying answer using just Coq's Print Assumptions command.
12+
13+
The exercise here is to implement an improved Print Assumptions command in Coq, such that
14+
15+
Compute print_assumptions ($quote_rec 0).
16+
17+
prints []
18+
19+
and
20+
21+
Axiom test : nat.
22+
23+
Compute print_assumptions ($quote_rec test).
24+
25+
prints a list containing a representation of test.
26+
27+
Define print_assumptions : global_env * term -> list kername
28+
*)
29+
30+
Load MetaCoqPrelude.
31+
(* if this does not work for you, compile the file using `coqc -I . "" MetaCoqPrelude`, and instead use the following line *)
32+
(* Require Import MetaCoqPrelude. *)
33+
34+
Unset Guard Checking.
35+
Section fix_Σ.
36+
37+
Variable (Σ : global_env).
38+
39+
End fix_Σ.
40+
Set Guard Checking.
41+
42+
(* Definition print_assumptions p := print_assms p.1 p.2. *)
43+
44+
(* Compute print_assumptions ($quote_rec 0). *)
45+
46+
Axiom test : nat.
47+
48+
(* Compute print_assumptions ($quote_rec test). *)
49+
50+
(* Module test. *)
51+
52+
(* Require Import Classical. *)
53+
54+
(* Lemma DNE P : ~~ P -> P. *)
55+
(* Proof. *)
56+
(* tauto. *)
57+
(* Qed. *)
58+
59+
(* End test. *)
60+
61+
(* Compute print_assumptions ($quote_rec test.DNE). *)
62+
63+
(** ** Define a function which replaces let binding by equivalent beta redexes
64+
65+
You can copy-paste and rename the below identity function as starting point.
66+
*)
67+
68+
Fixpoint identity (t : term) :=
69+
match t with
70+
| tRel n => tRel n
71+
| tVar id => tVar id
72+
| tEvar ev args => tEvar ev (map identity args)
73+
| tSort s => tSort s
74+
| tCast t kind v => tCast (identity t) kind (identity v)
75+
| tProd na ty body => tProd na (identity ty) (identity body)
76+
| tLambda na ty body => tLambda na (identity ty) (identity body)
77+
| tLetIn na def def_ty body => tLetIn na (identity def) (identity def_ty) (identity body)
78+
| tApp f args => tApp (identity f) (map identity args)
79+
| tConst c u => tConst c u
80+
| tInd ind u => tInd ind u
81+
| tConstruct ind idx u => tConstruct ind idx u
82+
| tCase ind p discr brs =>
83+
let p' := map_predicate id identity identity p in
84+
let brs' := map_branches identity brs in
85+
tCase ind p' (identity discr) brs'
86+
| tProj proj t => tProj proj (identity t)
87+
| tFix mfix idx => tFix (map (map_def identity identity) mfix) idx
88+
| tCoFix mfix idx => tCoFix (map (map_def identity identity) mfix) idx
89+
| tInt i => tInt i
90+
| tFloat f => tFloat f
91+
end.
92+
93+
(* Check $unquote (let_to_lambda (Mower 5)). *)
94+
95+
(** ** Define a function which replaces any subterm of form a * b + c by a call to muladd: *)
96+
97+
Definition muladd a b c := a * b + c.
98+
99+
Unset Guard Checking.
100+
101+
(* Check $unquote (fold_muladd ($quote (3 * 2 + 5))). *)
102+
103+
(* Check $unquote (fold_muladd ($quote (1 + (3 * 2 + 5)))). *)
104+
105+
(** ** Write a command reify that reifies Coq formulas into the following datatype *)
106+
107+
Inductive arith :=
108+
| aPlus : arith -> arith -> arith
109+
| aConst : nat -> arith.
110+
111+
(* Goal 4 + (3 + 1) = 2. *)
112+
(* Proof. *)
113+
(* match goal with *)
114+
(* | [ |- ?L = _ ] => pose ($unquote (reify ($quote L))) *)
115+
(* end. *)
116+
(* Abort. *)

‎popl24/live_coding.v‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
(** * MetaCoq *)
2+
3+
Load MetaCoqPrelude.
4+
5+
Print term.
6+
7+
Check $quote (fun x : nat => x).
8+
9+
Check $unquote (tLam "y" ($quote bool) ($quote (fun x : nat => x))).
10+
11+
Definition tNat := $quote nat.
12+
13+
Definition idNat := $unquote
14+
(tLam "x" tNat (tRel 0)).
15+
Print idNat.
16+
17+
Check $unquote (tLam "x" ($quote nat) (tRel 0)).
18+
19+
#[bypass_check(guard)]
20+
Fixpoint Mpower' (n : nat) : term :=
21+
match n with
22+
| 0 => $quote 1
23+
| 1 => tRel 0
24+
| 2 => tApp ($quote mult) [tRel 0; tRel 0]
25+
| S n' as n => if n mod 2 =? 0 then
26+
tLet "p" ($quote nat) (Mpower' (div n 2))
27+
(tApp ($quote mult) [tRel 0 ; tRel 0])
28+
else tApp ($quote mult) [Mpower' n' ; tRel 0]
29+
end.
30+
31+
Print Mpower'.
32+
33+
Definition Mpower (n : nat) :=
34+
tLam "x" ($quote nat) (Mpower' n).
35+
36+
Compute Mpower' 3.
37+
38+
Definition power3 := ($unquote (Mpower 3)).
39+
Print power3.
40+
41+
Definition power13 := ($unquote (Mpower 13)).
42+
Print power13.
43+
Print Assumptions power13.
44+
45+
Inductive arith :=
46+
| aPlus : arith -> arith -> arith
47+
| aConst : nat -> arith.
48+
49+
Fixpoint reify (x : term) :=
50+
match x with
51+
| tApp c [u; v] =>
52+
if c == $quote plus
53+
then tApp ($quote aPlus) [reify u; reify v]
54+
else tApp ($quote aConst) [x]
55+
| n => tApp ($quote aConst) [x]
56+
end.
57+
58+
Goal 4 + (3 + 1) = 2.
59+
Proof.
60+
match goal with
61+
| [ |- ?L = _ ] => pose ($unquote (reify ($quote L)))
62+
end.
63+
Abort.
64+
65+
(** ** Advanced *)
66+
(** Write automation that unfolds and reduces all constants c in a term, *unless* c : Type, or c : P where P : Prop.
67+
It suffices to change the tConst case of the function below. Use the auxiliary function defined and checked below.
68+
*)
69+
70+
Definition reduce Σ t := match reduce_opt RedFlags.default Σ [] default_fuel t with Some res => res | _ => t end.
71+
Definition infer_type Σ t := infer (cf := config.default_checker_flags) (F := default_fuel) Σ init_graph [] t.
72+
73+
Check lookup_constant.
74+
Check Universe.is_prop.
75+
76+
Require Import List.
77+
78+
Section fix_Sigma.
79+
80+
Variable Σ : global_env.
81+
82+
Fixpoint simplify_consts (t : term) :=
83+
match t with
84+
| tRel n => tRel n
85+
| tVar id => tVar id
86+
| tEvar ev args => tEvar ev (map simplify_consts args)
87+
| tSort s => tSort s
88+
| tCast t kind v => tCast (simplify_consts t) kind (simplify_consts v)
89+
| tProd na ty body => tProd na (simplify_consts ty) (simplify_consts body)
90+
| tLambda na ty body => tLambda na (simplify_consts ty) (simplify_consts body)
91+
| tLetIn na def def_ty body => tLetIn na (simplify_consts def) (simplify_consts def_ty) (simplify_consts body)
92+
| tApp f args => tApp (simplify_consts f) (map simplify_consts args)
93+
| tConst c u =>
94+
match infer_type Σ (tConst c u) with
95+
| Checked (tSort _) => tConst c u
96+
| Checked A =>
97+
match infer_type Σ A with
98+
| Checked (tSort univ) => if Universe.is_prop univ then
99+
tConst c u
100+
else
101+
match lookup_constant Σ c with
102+
| Some {| cst_body := Some b |} => reduce Σ b
103+
| _ => tConst c u
104+
end
105+
| Checked K => match lookup_constant Σ c with
106+
| Some {| cst_body := Some b |} => reduce Σ b
107+
| _ => tConst c u
108+
end
109+
| TypeError E => tConst c u
110+
end
111+
| TypeError E => tConst c u
112+
end
113+
| tInd ind u => tInd ind u
114+
| tConstruct ind idx u => tConstruct ind idx u
115+
| tCase ind p discr brs =>
116+
let p' := map_predicate id simplify_consts simplify_consts p in
117+
let brs' := map_branches simplify_consts brs in
118+
tCase ind p' (simplify_consts discr) brs'
119+
| tProj proj t => tProj proj (simplify_consts t)
120+
| tFix mfix idx => tFix (map (map_def simplify_consts simplify_consts) mfix) idx
121+
| tCoFix mfix idx => tCoFix (map (map_def simplify_consts simplify_consts) mfix) idx
122+
| tInt i => tInt i
123+
| tFloat f => tFloat f
124+
end.
125+
126+
End fix_Sigma.
127+
128+
Definition unfold_comp (p : program) :=
129+
simplify_consts p.1 p.2.
130+
131+
Definition dont := nat.
132+
Definition alsodont := conj I (fun x : False => x).
133+
Definition do := 3 + 1.
134+
135+
Check $unquote (unfold_comp ($quote_rec (dont, alsodont, do))).
136+
(* expected output: (dont, alsodont, 4) *)

0 commit comments

Comments
 (0)