https://github.com/c-corn/corn
Raw File
Tip revision: af4b86e6ad6cfd242562f9c33c0e438298fc4e1f authored by Théo Zimmermann on 07 September 2021, 14:21:48 UTC
Merge pull request #161 from Zimmi48/update-ci-8.13
Tip revision: af4b86e
Ranges.v

Require Import Program MathClasses.interfaces.canonical_names util.Container QArith QMinMax CRlattice.

Definition Range (T: Type) := prod T T.

Instance in_QRange: Container Q (Range Q)
  := λ r x, (Qmin (fst r) (snd r) <= x <= Qmax (fst r) (snd r))%Q.

Instance in_CRRange: Container (msp_car CR) (Range (msp_car CR))
  := λ r x,
     (ucFun (ucFun CRmin (fst r)) (snd r) <= x)%CR
     ∧ (x <= ucFun (ucFun CRmax (fst r)) (snd r))%CR.

Instance in_sig_Range `{Container A (Range A)} (P: A → Prop): Container (sig P) (Range (sig P))
  := λ r x, In (` (fst r), ` (snd r)) (` x).

back to top