search

FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

Compilation of projections is not clever ? #19

Open FissoreD opened 5 days ago

FissoreD commented 5 days ago

The compilation of ucmra_unit_left_id in iris gives the following elpi rule

(tc-stdpp.base.tc-LeftId A1 (app [global (const «equiv»), A2, A3]) 
  (app [global (const «ε»), A4, A5]) (app [global (const «op»), A6, A7]) 
  (app [global (const «ucmra_unit_left_id»), A0])) :- 
 (coq.unify-eq A7 (app [global (const «cmra_op»), app [global (const «ucmra_cmraR»), A0]]) ok), 
 (coq.unify-eq A6 (app [global (const «ucmra_car»), A0]) ok), 
 (coq.unify-eq A5 (app [global (const «ucmra_unit»), A0]) ok), 
 (coq.unify-eq A4 (app [global (const «ucmra_car»), A0]) ok), 
 (coq.unify-eq A3 (app [global (const «ofe_equiv»), app [global (const «ucmra_ofeO»), A0]]) ok), 
 (coq.unify-eq A2 (app [global (const «ucmra_car»), A0]) ok), 
 (coq.unify-eq A1 (app [global (const «ucmra_car»), A0]) ok).

Note that the type of ucmra_unit_left_id is

∀ {A : ucmra}, @LeftId 
  (ucmra_car A) 
  (@equiv (ucmra_car A) (ofe_equiv (ucmra_ofeO A))) 
  (@ε (ucmra_car A) (ucmra_unit A)) 
  (@op (ucmra_car A) (cmra_op (ucmra_cmraR A)))

all the ucmra_car A could be replaced with a unique coq.unify-eq The example could produce a elpi rule like:

(tc-stdpp.base.tc-LeftId A1 (app [global (const «equiv»), A2, A3]) 
  (app [global (const «ε»), A4, A5]) (app [global (const «op»), A6, A7]) 
  (app [global (const «ucmra_unit_left_id»), A0])) :- A6 = A4, A1 = A4, A2 = A1,
 (coq.unify-eq A7 (app [global (const «cmra_op»), app [global (const «ucmra_cmraR»), A0]]) ok), 
 (coq.unify-eq A6 (app [global (const «ucmra_car»), A0]) ok), 
 (coq.unify-eq A5 (app [global (const «ucmra_unit»), A0]) ok), 
 (coq.unify-eq A3 (app [global (const «ofe_equiv»), app [global (const «ucmra_ofeO»), A0]]) ok)).
FissoreD commented 5 days ago

However, I'm not completely sure that the second implementation will work in all cases. I think there could be two non-unfiable terms (for elpi at least) that however unify for coq. For example, there could exists two terms $t_1$ and $t_2$ assigned to $A6$ and $A4$ such that $t_1 \neq t_2$ in elpi where coq.unify-eq A4 A6 would actually succeed