rename rules -> op_rules

Really, *all* of our files contain proof rules

_CoqProject

@@ -96,7 +96,7 @@ program_logic/ownp.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
-heap_lang/rules.v
+heap_lang/op_rules.v
 heap_lang/notation.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v

heap_lang/adequacy.v

 From iris.program_logic Require Export weakestpre adequacy gen_heap.
-From iris.heap_lang Require Export rules.
+From iris.heap_lang Require Export op_rules.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.

heap_lang/lib/lock.v

-From iris.heap_lang Require Export rules notation.
+From iris.heap_lang Require Export op_rules notation.
 From iris.base_logic.lib Require Export invariants.
 
 Structure lock Σ `{!heapG Σ} := Lock {

heap_lang/rules.v → heap_lang/op_rules.v

@@ -6,6 +6,8 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
 Import uPred.
 
+(** Basic rules for language operations. *)
+
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ

heap_lang/proofmode.v

 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
-From iris.heap_lang Require Export wp_tactics rules.
+From iris.heap_lang Require Export wp_tactics op_rules.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.

heap_lang/wp_tactics.v

-From iris.heap_lang Require Export tactics rules.
+From iris.heap_lang Require Export tactics op_rules.
 Import uPred.
 
 (** wp-specific helper tactics *)

[Robbert Krebbers]

But op rules makes even less sense... Then call it wp_rules?

[Robbert Krebbers]

Now it looks like this file is specific to bin_op and un_op or so.

[Ralf Jung]

But op rules makes even less sense...

It certainly makes more sense than just "rules". I agree it may not be perfect.

Then call it wp_rules?

Containing rules for WP is hardly a distinguishing feature of this file. What about lang_wp or wp_lang?

[Robbert Krebbers]

I think rules covers it fairly well, this file contains the core proof rules of the language. All the other stuff is just derived on top of that.

But since you don't like it, how about just weakestpre by analogy to program_logic/weakestpre. Or alternatively, base_rules.

[Ralf Jung]

You said it quite well -- the core proof rules of the language, in contrast to the core proof rules of a lock or sth. I think that should be expressed in the name.

[Robbert Krebbers]

It is in the root of the folderheap_lang, that should make that clear.

[Ralf Jung]

Well, we also have a file lang.v. What is your problem with wp_lang/lang_wp? IMHO that conveys the content quite well.

Cc @jjourdan

[Jacques-Henri Jourdan]

First of all, @jung, I don't quite see how op_rules makes more sense than rules. I don't see what op refers to : operational? operators? Then, I don't like wp_lang or lang_wp, because heap_lang/lang_wp is redundant.

So, now, I like weakestpre or wp. We could even go back to lifting, which, I think, was quite a good name.

[Robbert Krebbers]

JH precisely describes my concerns. We then also have to prefix all the other files with lang_.

I am not so sure whether lifting still makes sense, program_logic/lifting contains the generic lifting lemmas/rules, whereas this file just makes use of it.

[Jacques-Henri Jourdan]

I am not so sure whether lifting still makes sense, program_logic/lifting contains the generic lifting lemmas/rules, whereas this file just makes use of it.

That is the point : in a sense, this file specializes the lifting lemmas to this language.

[Ralf Jung]

op is for operational. But okay, if you both don't like it, then let's look for sth. else.

heap_lang contains lots of things related to the language, the primitive language-specific triples are fairly particular. I think that justifies having lang twice, like it is twice in heap_lang.lang.

[Jacques-Henri Jourdan]

op is for operational. But okay, if you both don't like it, then let's look for sth. else.

Ok. But the point is that here we are not describing the operational semantics, but rather an axiomatic semantic. rules_op would probably be more appropriate for the current lang.v.

heap_lang contains lots of things related to the language, the primitive language-specific triples are fairly particular. I think that justifies having lang twice, like it is twice in heap_lang.lang.

I am not too strongly opposed to wp_lang. Enven though weakestpre or lifting would make more sens in my opinion.

[Robbert Krebbers]

My preferences:

1. rules
2. weakestpre
3. lifting
4. lang_rules
5. lang_weakestpre

I will veto against rules_op.

[Ralf Jung]

1. lang_wp
2. lang_weakestpre
3. lifting
4. {base,basic}_{wp,weakestpre}

I will veto anything involving "rules" (I am aware this includes vetoing the current name; the reason I used it is that I wanted to stick to the term you used but make it more descriptive). I could maybe accept just "weakestpre", but I still think it is a horribly indescriptive name.

[Robbert Krebbers]

Alright, then let's go back to lifting as the file was called before. JH seems to prefer that name, and it is the first common name on both of our lists.

[Ralf Jung]

Ack. Will do.