Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use nested recursion for fresh variables #10

Merged
merged 2 commits into from
Jan 25, 2024
Merged

Use nested recursion for fresh variables #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1da5218
use nested recursion to handle fresh variable predicate using Equations
palmskog Jan 25, 2024
7c37583
let's try to use Dune in CI/opam for some extra testing
palmskog Jan 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions coq-abs-metatheory.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ synopsis: "Formal metatheory in Coq of the ABS language"
description: """
Formal metatheory in Coq for the ABS language."""

build: [make "-j%{jobs}%"]
install: [make "install"]
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "3.5"}
"coq" {>= "8.16"}
"coq-ott" {>= "0.33"}
"coq-equations" {>= "1.3"}
Expand Down
26 changes: 8 additions & 18 deletions src/abs.ott
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ formula :: formula_ ::=
| G ( fn ) = sig :: M :: G_fn_eq_sig
{{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }}
| fresh ( x1 , ... , xn , e ) :: M :: fresh
{{ coq (fresh_vars [[x1 ... xn]] [[e]]) }}
{{ coq (fresh_vars_e [[x1 ... xn]] [[e]]) }}

embed
{{ coq
Expand All @@ -135,23 +135,13 @@ Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
e_fn_call fn (map (fun e => e_var_subst e l) e_list)
end.

(* we actually need to do some work to convince Coq fresh_vars is well founded *)
Fixpoint e_size (e0 : e) : nat :=
match e0 with
| e_t _ => 1
| e_var _ => 1
| e_fn_call _ es => 1 + list_sum (map e_size es)
end.

Equations fresh_vars (l : list x) (e0 : e) : Prop by wf (e_size e0) lt :=
fresh_vars _ (e_t _) := True;
fresh_vars l (e_var x) := ~ In x l;
fresh_vars _ (e_fn_call fn nil) := True;
fresh_vars l (e_fn_call fn (e1::es)) :=
fresh_vars l e1 /\ fresh_vars l (e_fn_call fn es).
Next Obligation. lia. Qed.
Next Obligation. destruct e1;cbn;lia. Qed.

Equations fresh_vars_e (l : list x) (e0 : e) : Prop := {
fresh_vars_e _ (e_t _) := True;
fresh_vars_e l (e_var x) := ~ In x l;
fresh_vars_e l (e_fn_call fn el) := fresh_vars_el l el }
where fresh_vars_el (l : list x) (el0 : list e) : Prop := {
fresh_vars_el l nil := True;
fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }.
}}

defns
Expand Down
26 changes: 8 additions & 18 deletions theories/abs_defs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,23 +122,13 @@ Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
e_fn_call fn (map (fun e => e_var_subst e l) e_list)
end.

(* we actually need to do some work to convince Coq fresh_vars is well founded *)
Fixpoint e_size (e0 : e) : nat :=
match e0 with
| e_t _ => 1
| e_var _ => 1
| e_fn_call _ es => 1 + list_sum (map e_size es)
end.

Equations fresh_vars (l : list x) (e0 : e) : Prop by wf (e_size e0) lt :=
fresh_vars _ (e_t _) := True;
fresh_vars l (e_var x) := ~ In x l;
fresh_vars _ (e_fn_call fn nil) := True;
fresh_vars l (e_fn_call fn (e1::es)) :=
fresh_vars l e1 /\ fresh_vars l (e_fn_call fn es).
Next Obligation. lia. Qed.
Next Obligation. destruct e1;cbn;lia. Qed.

Equations fresh_vars_e (l : list x) (e0 : e) : Prop := {
fresh_vars_e _ (e_t _) := True;
fresh_vars_e l (e_var x) := ~ In x l;
fresh_vars_e l (e_fn_call fn el) := fresh_vars_el l el }
where fresh_vars_el (l : list x) (el0 : list e) : Prop := {
fresh_vars_el l nil := True;
fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }.

(** definitions *)

Expand Down Expand Up @@ -174,7 +164,7 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop := (* defn e *)
red_e F_list s5 e_5 s' e' ->
red_e F_list s5 (e_fn_call fn5 ((app e_list (app (cons e_5 nil) (app e'_list nil))))) s' (e_fn_call fn5 ((app e_list (app (cons e' nil) (app e'_list nil)))))
| red_fun_ground : forall (T_x_t_y_list:list (T*x*t*x)) (F'_list F_list:list F) (T_5:T) (fn5:fn) (e5:e) (s5:s),
(fresh_vars (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 ) ->
(fresh_vars_e (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 ) ->
red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list)) (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5) s5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) ) (e_var_subst e5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) .


Loading