From 4a614ba7e6e733d1adc7f4998ac5ae5d7a4a19e4 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 12 Apr 2023 14:15:56 +0200
Subject: [PATCH 1/2] Handle casts in lra parser

---
 examples/lra_examples.v | 5 +++++
 theories/lra.elpi       | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/examples/lra_examples.v b/examples/lra_examples.v
index ff7f7b1..63f9689 100644
--- a/examples/lra_examples.v
+++ b/examples/lra_examples.v
@@ -36,6 +36,11 @@ Variable F : realFieldType.
 
 Implicit Types x y : F.
 
+Lemma test_cast : 0 <= 2 :> F.
+Proof.
+lra.
+Qed.
+
 Lemma test_lt x y :
   x + 2%:R * y < 3%:R -> 2%:R * x + y <= 3%:R -> x + y < 2%:R.
 Proof.
diff --git a/theories/lra.elpi b/theories/lra.elpi
index cbdc53b..6afd788 100644
--- a/theories/lra.elpi
+++ b/theories/lra.elpi
@@ -177,6 +177,9 @@ quote.int {{ Negz lp:N }} {{ large_int_Z (Zneg lp:P) }} (coqZneg P) :-
 % - [VM] is a variable map, that is a list of terms of type [R].
 pred quote.expr i:bool, i:term, i:option term, i:term, i:option term,
     i:(term -> term), i:term, o:term, o:term, o:list term.
+% _ : _
+quote.expr ff R F TR TUR Morph {{ lp:E : _ }} OutM Out VM :- !,
+  quote.expr ff R F TR TUR Morph E OutM Out VM.
 % 0%R
 quote.expr _ R _ _ _ _ {{ @GRing.zero lp:U }}
            {{ @R0 lp:R }} {{ PEc (Qmake 0 1) }} _ :-

From ec0fc7e03e92a572d5b0f6129d8912b4d068bc64 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 12 Apr 2023 14:19:34 +0200
Subject: [PATCH 2/2] Add a few lra examples

---
 examples/lra_examples.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/examples/lra_examples.v b/examples/lra_examples.v
index 63f9689..1249fe8 100644
--- a/examples/lra_examples.v
+++ b/examples/lra_examples.v
@@ -41,6 +41,11 @@ Proof.
 lra.
 Qed.
 
+Example test_div x y : x / 2 + y <= 3 -> x + y / 2 <= 3 -> x + y <= 4.
+Proof.
+lra.
+Qed.
+
 Lemma test_lt x y :
   x + 2%:R * y < 3%:R -> 2%:R * x + y <= 3%:R -> x + y < 2%:R.
 Proof.
@@ -294,3 +299,11 @@ lra.
 Qed.
 
 End TestsCoq.
+
+Example test_abstract_rmorphism (R : realDomainType) (f : {rmorphism R -> R})
+  (x y : R) : f y >= 0 -> f x + 2 * f (y + 1) <= f (3 * y + x) + 2.
+Proof. lra. Qed.
+
+Example test_concrete_rmorphism (R : realFieldType) (x y : rat) :
+  ratr y >= 0 :> R -> ratr x + 2 * ratr (y + 1) <= ratr (3 * y + x) + 2 :> R.
+Proof. lra. Qed.