[Agda] ⊓ in Nat

[Andreas Abel]

Dear Sergei,

well, there is

m⊓n≤m : ∀ m n → m ⊓ n ≤ m
m⊓n≤m zero    _       = z≤n
m⊓n≤m (suc m) zero    = z≤n
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n

and there is commutativity of the minium.

isDistributiveLattice : IsDistributiveLattice _≡_ _⊓_ _⊔_
isDistributiveLattice = record
   { isLattice = record
       { isEquivalence = PropEq.isEquivalence
       ; ∨-comm        = ⊓-comm
       ; ∨-assoc       = ⊓-assoc
       ; ∨-cong        = cong₂ _⊓_
       ; ∧-comm        = ⊔-comm
       ; ∧-assoc       = ⊔-assoc
       ; ∧-cong        = cong₂ _⊔_
       ; absorptive    = absorptive-⊓-⊔
       }
   ; ∨-∧-distribʳ = proj₂ distrib-⊓-⊔
   }

Together, you get what you need.

Best,
Andreas

On 22.04.2017 12:49, Sergei Meshveliani wrote:
> Dear list,
>
> This is on Standard library.
>
> Data.Nat  defines _⊓_,  and Data.Nat.Properties proves certain
> properties of _⊓_.
> And I have an impression that it lacks a lemma
>
>   ⊓≤both :  ∀ m n →  m ⊓ n ≤ m  ×  m ⊓ n ≤ n
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/