Skip to content

Changed reduction to mirror behaviour of native Rocq encodings #64

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

Merged
fblanqui merged 6 commits into from
Jul 8, 2026
Merged

Changed reduction to mirror behaviour of native Rocq encodings #64

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b5239aa
Changed reduction
melanie-taprogge Jun 29, 2026
b588b14
fixes
melanie-taprogge Jun 29, 2026
a344881
cosmetic fixes
melanie-taprogge Jun 30, 2026
0439f60
Merge remote-tracking branch 'dk/master' into rocq-compatible-version
fblanqui Jul 8, 2026
f1dc383
rename Reduction to ExtraRules, and update CHANGES.md
fblanqui Jul 8, 2026
ca4342a
details
fblanqui Jul 8, 2026
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
24 changes: 19 additions & 5 deletions Bool.lp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,9 +111,23 @@ symbol or : 𝔹 → 𝔹 → 𝔹;
notation or infix left 20;

rule true or _ ↪ true
with _ or true ↪ true
with false or $b ↪ $b
with $b or false ↪ $b;
with false or $b ↪ $b;

opaque symbol or_true_lhs [p : 𝔹] :
π ((p or true) = true) ≔
begin
induction
{reflexivity}
{reflexivity}
end;

opaque symbol or_false_lhs [p : 𝔹] :
π ((p or false) = p) ≔
begin
induction
{reflexivity}
{reflexivity}
end;

opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
begin
Expand Down Expand Up @@ -154,8 +168,8 @@ end;
opaque symbol orC p q : π (p or q = q or p) ≔
begin
induction
{ reflexivity; }
{ reflexivity; }
{ assume q; rewrite or_true_lhs [q]; reflexivity }
{ assume q; rewrite or_false_lhs [q]; reflexivity }
end;

opaque symbol orA p q r : π ((p or q) or r = p or (q or r)) ≔
Expand Down
7 changes: 7 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,13 @@ All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](https://keepachangelog.com/),
and this project adheres to [Semantic Versioning](https://semver.org/).

## Unreleased

### Changed

- Changed rewrite rules to be in line with the Rocq standard library.
- Moved rules not in line with Rocq to the module ExtraRules.

## 1.4.0 (2026-07-07)

### Added
Expand Down
45 changes: 45 additions & 0 deletions ExtraRules.lp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// This module turns proved equalities to rewrite rules

@fblanqui fblanqui Jun 30, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I propose to rename the file to ExtraRules.lp and move the require commands as follows:

// rules from Bool

require Stdlib.Bool as B;

rule _ B.or B.true  ↪ B.true
with $b B.or B.false ↪ $b;

// rules from Nat

require Stdlib.Nat as N;

...

require open Stdlib.Bool;
require Stdlib.Nat as N;
Comment thread
fblanqui marked this conversation as resolved.
require open Stdlib.List;
require Stdlib.Pos as P;
require Stdlib.Z as Z;

// Bool

rule _ or true ↪ true
with $b or false ↪ $b;

// Nat

rule $x N.+ N._0 ↪ $x;
rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
rule ($x N.+ $y) N.+ $z ↪ $x N.+ ($y N.+ $z);
rule $x N.- N._0 ↪ $x;
rule _ N.* N._0 ↪ N._0;
rule N.max $x N._0 ↪ $x;
rule N.max $x $x ↪ $x;
rule N.min _ N._0 ↪ N._0;
rule N.min $x $x ↪ $x;

// List

rule $m ++ □ ↪ $m;
rule size ($l ++ $m) ↪ size $l N.+ size $m;
rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
rule last _ ($e ⸬ $l) ↪ last $e $l;
rule nth $x □ _ ↪ $x;
rule drop _ □ ↪ □;
rule take _ □ ↪ □;

// Pos

rule P.add $x P.H ↪ P.succ $x
with P.add P.H $y ↪ P.succ $y;
rule P.add_carry $x P.H ↪ P.add $x (P.O P.H)
with P.add_carry P.H $y ↪ P.add (P.O P.H) $y;

// Z

rule $x Z.+ Z.Z0 ↪ $x;
100 changes: 66 additions & 34 deletions List.lp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -403,8 +403,6 @@ begin
{ assume x l' h; simplify; rewrite h; reflexivity; }
end;

rule $m ++ □ ↪ $m;

opaque symbol size_cat [a] (l m : 𝕃 a) : π(size (l ++ m) = size l + size m) ≔
begin
assume a;
Expand All @@ -415,8 +413,6 @@ begin
{ assume x l' h m; simplify; rewrite h; reflexivity; }
end;

rule size ($l ++ $m) ↪ size $l + size $m;

opaque symbol catA [a] (l m n : 𝕃 a) : π((l ++ m) ++ n = l ++ (m ++ n)) ≔
begin
assume a;
Expand All @@ -427,8 +423,6 @@ begin
{ assume x l' h m n; simplify; rewrite h; reflexivity; }
end;

rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);

opaque symbol cat_nilp [a] (l1 l2 : 𝕃 a) :
π (nilp (l1 ++ l2) = (nilp l1 and nilp l2)) ≔
begin
Expand All @@ -454,24 +448,24 @@ opaque symbol catrev_cat [a] (l m:𝕃 a): π(catrev l m = rev l ++ m) ≔
begin
assume a; induction
{ reflexivity }
{ assume x l ih m; simplify; rewrite ih; rewrite ih (x ⸬ □); reflexivity }
{ assume x l ih m; simplify; rewrite ih; rewrite ih (x ⸬ □); rewrite catA; reflexivity }
end;

opaque symbol rev_cons [a] l (x:τ a): π(rev (x ⸬ l) = rev l ++ (x ⸬ □)) ≔
begin
assume a; induction
{ reflexivity }
{ assume y l ih x; simplify; rewrite catrev_cat; rewrite catrev_cat l (y ⸬ □); reflexivity }
{ assume y l ih x; simplify; rewrite catrev_cat; rewrite catrev_cat l (y ⸬ □); rewrite catA; reflexivity }
end;

opaque symbol rev_cat [a] (l m : 𝕃 a) : π(rev (l ++ m) = rev m ++ rev l) ≔
begin
assume a;
induction
// case l = □
{ simplify; reflexivity; }
{ assume l; simplify; rewrite cats0; reflexivity }
// case l = ⸬
{ assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; reflexivity; }
{ assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; rewrite catA; reflexivity; }
end;

opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
Expand All @@ -487,7 +481,8 @@ begin
// case l = □
{ reflexivity }
// case l = ⸬
{ assume x l h; rewrite rev_cons; rewrite size_cat; rewrite h; reflexivity }
{ assume x l h; rewrite rev_cons; rewrite size_cat; rewrite h; simplify;
rewrite suc=+1; rewrite suc=+1; rewrite add0n; reflexivity}
end;

// rcons
Expand Down Expand Up @@ -549,11 +544,20 @@ assert x ⊢ indexes (x ⸬ x ⸬ x ⸬ x ⸬ □) ≡ 0 ⸬ 1 ⸬ 2 ⸬ 3 ⸬
symbol last [a] : τ a → 𝕃 a → τ a;

rule last $x □ ↪ $x
with last _ ($e ⸬ $l) ↪ last $e $l;
with last _ ($e ⸬ □) ↪ $e
with last $x (_ ⸬ ($e ⸬ $l)) ↪ last $x ($e ⸬ $l);

assert ⊢ last 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 1;
assert ⊢ last 4 □ ≡ 4;

opaque symbol lastl [a : Set] (l : 𝕃 a) (x y : τ a): π ((last x (y ⸬ l)) = last y l)≔
begin
assume a;
induction
{reflexivity}
{assume p l h x y; simplify; rewrite h; rewrite h; reflexivity}
end;

// belast

symbol belast [a] : τ a → 𝕃 a → 𝕃 a;
Expand All @@ -567,7 +571,8 @@ assert ⊢ belast 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 4 ⸬ 3 ⸬ 2 ⸬ □;

symbol nth [a] : τ a → 𝕃 a → ℕ → τ a;

rule nth $x □ _ ↪ $x
rule nth $x □ 0 ↪ $x
with nth $x □ (_ +1) ↪ $x
with nth _ ($e ⸬ _) 0 ↪ $e
with nth $x (_ ⸬ $l) ($n +1) ↪ nth $x $l $n;

Expand All @@ -576,6 +581,13 @@ assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 2 ≡ 1;
assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 3 ≡ 4;
assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 42 ≡ 4;

opaque symbol nthx□ [a: Set] n (x : τ a) : π((nth x □ n) = x)≔
begin
assume n; induction
{reflexivity}
{assume m h x; reflexivity;}
end;

// set_nth

symbol set_nth [a] : τ a → 𝕃 a → ℕ → τ a → 𝕃 a;
Expand Down Expand Up @@ -723,7 +735,7 @@ begin
assume a b x y; induction
{ assume lb i h;
have t: π (lb = □) { apply size0nil lb; symmetry; apply h; };
rewrite t; reflexivity; }
rewrite t; simplify; rewrite nthx□; rewrite nthx□; rewrite nthx□; reflexivity}
{ assume ea la h; induction
{ assume i j; apply ⊥ₑ (s≠0 j); }
{ assume eb lb k; induction
Expand Down Expand Up @@ -752,12 +764,20 @@ end;
symbol drop [a] : ℕ → 𝕃 a → 𝕃 a;

rule drop 0 $l ↪ $l
with drop _ □ ↪ □
with drop (_ +1) □ ↪ □
with drop ($n +1) (_ ⸬ $l) ↪ drop $n $l;

assert ⊢ drop 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 1 ⸬ 41 ⸬ □;
assert ⊢ drop 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ □;

opaque symbol dropx□ [a: Set] n: π (drop n (□ [a]) = □)≔
begin
assume a;
induction
{reflexivity}
{reflexivity}
end;

opaque symbol drop0 [a] (l:𝕃 a) : π (drop 0 l = l) ≔
begin
reflexivity;
Expand Down Expand Up @@ -792,7 +812,7 @@ end;
opaque symbol size_drop [a] (l:𝕃 a) n : π (size (drop n l) = size l - n) ≔
begin
assume a; induction
{ reflexivity; }
{ assume n; rewrite dropx□; reflexivity}
{ assume e l h; simplify; induction
{ reflexivity; }
{ assume n i; simplify; apply h n; }
Expand Down Expand Up @@ -828,10 +848,11 @@ opaque symbol drop_drop [a] (l:𝕃 a) n1 n2 :
π (drop n1 (drop n2 l) = drop (n1 + n2) l) ≔
begin
assume a; induction
{ reflexivity; }
{ assume n m; rewrite dropx□; rewrite dropx□;
rewrite dropx□; reflexivity }
{ assume e l h n1; induction
{ reflexivity; }
{ assume n2 i; simplify; apply h n1 n2; }
{ simplify; rewrite addn0; reflexivity; }
{ assume n2 i; simplify; rewrite addnS; apply h n1 n2; }
}
end;

Expand All @@ -840,12 +861,20 @@ end;
symbol take [a] : ℕ → 𝕃 a → 𝕃 a;

rule take 0 _ ↪ □
with take _ □ ↪ □
with take (_ +1) □ ↪ □
with take ($n +1) ($x ⸬ $l) ↪ $x ⸬ (take $n $l);

assert ⊢ take 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ □;
assert ⊢ take 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □;

opaque symbol taken□ [a: Set] n: π (take n (□ [a]) = □)≔
begin
assume a;
induction
{reflexivity}
{reflexivity}
end;

opaque symbol take0 [a] (l: 𝕃 a) : π (take 0 l = □) ≔
begin
reflexivity;
Expand Down Expand Up @@ -943,10 +972,10 @@ begin
}
}
{ assume n h; induction
{ reflexivity; }
{ assume l; rewrite addn0; reflexivity }
{ assume m i; induction
{ reflexivity; }
{ assume e l j; simplify; apply i l; }
{ assume e l j; simplify; rewrite addnS; apply i l; }
}
}
end;
Expand All @@ -957,10 +986,10 @@ begin
assume a; induction
{ reflexivity; }
{ assume m h; induction
{ reflexivity; }
{ assume l; simplify; rewrite addn0; rewrite cats0; reflexivity }
{ assume n i; induction
{ reflexivity; }
{ assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l);
{ assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l); rewrite addnS;
rewrite left addnS; apply h (n +1) l; }
}
}
Expand All @@ -970,9 +999,9 @@ opaque symbol takeC [a] (l:𝕃 a) i j:
π (take i (take j l) = take j (take i l)) ≔
begin
assume a; induction
{ reflexivity; }
{ assume i j; rewrite taken□; rewrite taken□; rewrite taken□; reflexivity}
{ assume e l h; induction
{ reflexivity; }
{ assume i; simplify; rewrite taken□; reflexivity }
{ assume i h2; induction
{ reflexivity; }
{ assume j h3; simplify; rewrite h i j; reflexivity; }
Expand All @@ -993,12 +1022,12 @@ end;

opaque symbol rot0 [a] (l:𝕃 a) : π (rot 0 l = l) ≔
begin
reflexivity;
assume a l; simplify; rewrite cats0; reflexivity
end;

opaque symbol size_rot [a] (l:𝕃 a) n0 : π (size (rot n0 l) = size l) ≔
begin
assume a l n0; simplify; rewrite addnC;
assume a l n0; simplify; rewrite size_cat; rewrite addnC;
rewrite left @size_cat a (take n0 l) (drop n0 l);
rewrite cat_take_drop n0 l; reflexivity;
end;
Expand Down Expand Up @@ -1051,7 +1080,7 @@ end;

opaque symbol rotr0 [a] (l:𝕃 a) : π (rotr 0 l = l) ≔
begin
assume a l; simplify; rewrite take_size l; rewrite @drop_size a; reflexivity;
assume a l; simplify; rewrite sub0n; rewrite take_size l; rewrite @drop_size a; reflexivity;
end;

// membership
Expand All @@ -1076,7 +1105,9 @@ end;

opaque symbol mem_seq1 [a] beq (x y:τ a) : π (∈ beq x (y ⸬ □) = beq x y) ≔
begin
assume a beq x y; reflexivity;
assume a beq x y;
simplify; rewrite or_false_lhs [beq x y];
reflexivity;
end;

opaque symbol mem_cat [a] beq (x:τ a) l1 l2 :
Expand Down Expand Up @@ -1190,7 +1221,8 @@ opaque symbol not_mem_cons_head [a] (beq : τ a → τ a → 𝔹) l l0 x:
begin
assume a beq;
induction
{assume x l0 h; refine h}
{assume x l0; simplify ∈;
rewrite or_false_lhs [beq l0 x]; assume h; refine h}
{assume x l h0 l0 l1 h1 h2;
have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
{rewrite istrue=true h2; simplify; assume h3; refine h3 ⊤ᵢ};
Expand All @@ -1205,7 +1237,7 @@ begin
{assume x l0 h0 h1; refine h1}
{assume x l h0 l0 l1 h1 h2;
have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
{rewrite istrue=true h2; simplify; assume h3; refine h3 ⊤ᵢ};
{rewrite istrue=true h2; rewrite or_true_lhs [beq l1 l0]; simplify; assume h3; refine h3 ⊤ᵢ};
refine H0 h1}
end;

Expand Down Expand Up @@ -1502,7 +1534,7 @@ begin
refine ind_𝔹 (λ b:𝔹, (filter p (rev l) ++ (if b (e ⸬ □) □) = rev (if b (e ⸬ filter p l) (filter p l)))) _ _ (p e) {
simplify; rewrite catrev_cat (filter p l) (e ⸬ □); rewrite left h; reflexivity;
} {
simplify; rewrite left rev_def; rewrite h; reflexivity;
simplify; rewrite left rev_def; rewrite h; rewrite cats0; reflexivity;
};
}
end;
Expand Down Expand Up @@ -1707,7 +1739,7 @@ opaque symbol last_map [a b] (f:τ a → τ b) l x :
begin
assume a b f; induction
{ reflexivity; }
{ assume e l h x; simplify; rewrite h e; reflexivity; }
{ assume e l h x; simplify; rewrite lastl; rewrite lastl; rewrite h e; reflexivity; }
end;

opaque symbol belast_map [a b] (f:τ a → τ b) l x :
Expand Down
Loading