Merge pull request #9 from kth-step/equations-in-fresh

Equations for fresh_vars

README.md

@@ -22,6 +22,7 @@ Formal metatheory in Coq for the ABS language.
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
   - [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
+  - [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
 - Coq namespace: `ABS`
 - Related publication(s):
   - [ABS: A Core Language for Abstract Behavioral Specification](https://link.springer.com/chapter/10.1007/978-3-642-25271-6_8) doi:[10.1007/978-3-642-25271-6_8](https://doi.org/10.1007/978-3-642-25271-6_8)

coq-abs-metatheory.opam

@@ -14,11 +14,12 @@ synopsis: "Formal metatheory in Coq of the ABS language"
 description: """
 Formal metatheory in Coq for the ABS language."""
 
-build: ["dune" "build" "-p" name "-j" jobs]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
 depends: [
-  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-ott" {>= "0.33"}
+  "coq-equations" {>= "1.3"}
 ]
 
 tags: [

meta.yml

@@ -34,6 +34,12 @@ dependencies:
   description: |-
     [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
 
+- opam:
+    name: coq-equations
+    version: '{>= "1.3"}'
+  description: |-
+    [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
+
 tested_coq_opam_versions:
 - version: '8.18'
 - version: '8.17'

src/abs.ott

@@ -4,7 +4,7 @@ Require Export Ascii.
 Require Export String.
 Require Export ZArith.
 Require Import Lia.
-Require Coq.Program.Wf.
+From Equations Require Import Equations.
 
 Require Import FMapList OrderedTypeEx.
 Module Map <: FMapInterface.S := FMapList.Make String_as_OT.
@@ -143,25 +143,14 @@ Fixpoint e_size (e0 : e) : nat :=
   | e_fn_call _ es => 1 + list_sum (map e_size es)
   end.
 
-Lemma size_ge_1: forall e0,
-     1 <= e_size e0.
-Proof. destruct e0;cbn;lia. Qed.
-
-Program Fixpoint fresh_vars (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
-  match e0 with
-  | e_t _ => True
-  | e_var x => ~ In x l
-  | e_fn_call fn es =>
-      match es with
-      | nil => True
-      | e1::es' => fresh_vars l e1
-                 /\ fresh_vars l (e_fn_call fn es')
-      end
-  end.
-Next Obligation. cbn;lia. Qed.
-Next Obligation.
-  induction es';cbn; specialize (size_ge_1 e1);intro; lia.
-Qed.
+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.
 
 }}
 

theories/abs_defs.v

@@ -10,7 +10,7 @@ Require Export Ascii.
 Require Export String.
 Require Export ZArith.
 Require Import Lia.
-Require Coq.Program.Wf.
+From Equations Require Import Equations.
 
 Require Import FMapList OrderedTypeEx.
 Module Map <: FMapInterface.S := FMapList.Make String_as_OT.
@@ -130,25 +130,14 @@ Fixpoint e_size (e0 : e) : nat :=
   | e_fn_call _ es => 1 + list_sum (map e_size es)
   end.
 
-Lemma size_ge_1: forall e0,
-     1 <= e_size e0.
-Proof. destruct e0;cbn;lia. Qed.
-
-Program Fixpoint fresh_vars (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
-  match e0 with
-  | e_t _ => True
-  | e_var x => ~ In x l
-  | e_fn_call fn es =>
-      match es with
-      | nil => True
-      | e1::es' => fresh_vars l e1
-                 /\ fresh_vars l (e_fn_call fn es')
-      end
-  end.
-Next Obligation. cbn;lia. Qed.
-Next Obligation.
-  induction es';cbn; specialize (size_ge_1 e1);intro; lia.
-Qed.
+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.
 
 
 (** definitions *)