Conjecture: record concatenation is safe with an open record on the left

[jeromesimeon]

The idea behind the conjecture:

Fields on the right of OpRecConcat hides corresponding fields that may exist on the left, so the type of those fields on the left do not matter.

Currently: if they are known in the left record type, the right field take precedence. For instance:

[a: Integer, b: String]++[a: String, c: Integer] -> [a: String,  b: String, c:Integer]

If the left record is open, the following should be sound:

[a: Integer, b: String, ..]++[a: String, c:Integer] -> [a: String, b: String, c:Integer, ..]

If c is present in the instance of the left, this will be hidden so we know the result of concatenation has a field c of type Integer

[jeromesimeon]

A bit of news on this:

The idea behind the conjecture:

Fields on the right of OpRecConcat hides corresponding fields that may exist on the left, so the type of those fields on the left do not matter.

Currently: if they are known in the left record type, the right field take precedence. For instance:

[a: Integer, b: String]++[a: String, c: Integer] -> [a: String,  b: String, c:Integer]

We currently have a property

qcert/coq/Utils/Bindings.v

Line 1689 in 4095ca2

Lemma edot_fresh_concat {A} x (d:A) b :

showing:

  Lemma edot_fresh_concat {A} x (d:A) b :
    ~ In x (domain b) ->
    edot (rec_concat_sort b ((x,d)::nil)) x = Some d.
  Proof.
    intros.
    apply (@assoc_lookupr_insertion_sort_fresh string ODT_string); trivial.
  Qed.

But something much stronger holds, which AFAICT was not proven yet:

  Lemma edot_concat_right {A} x (d:A) b c :
    edot c x = Some d ->
    edot (rec_concat_sort b c) x = Some d.
  Proof.
    intros.
    unfold rec_concat_sort.
    unfold edot in *.
    rewrite assoc_lookupr_drec_sort.
    simpl.
    induction b; simpl; auto.
    destruct a; simpl.
    rewrite IHb.
    reflexivity.
  Qed.

Which I think means that it does not matter whether the left record is open or closed.