//! Core typeclass for epistemic calculi.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Basic + Axioms
//! Paper: Aambø, arXiv:2603.04188, Definitions 3.1, 3.2
//!
//! An epistemic calculus is a non-trivial unital symmetric monoidal posetal
//! category: a partial order with a commutative, associative, monotone fusion
//! operation and a unit element.

/// Trait representing an epistemic calculus (Definition 3.1).
///
/// # Laws (verified in Lean 4)
/// - `fusion` is commutative: `fusion(x, y) = fusion(y, x)`
/// - `fusion` is associative: `fusion(fusion(x, y), z) = fusion(x, fusion(y, z))`
/// - `fusion` has a unit: `fusion(unit, x) = x`
/// - `fusion` is monotone: `x <= x' ∧ y <= y' ⟹ fusion(x, y) <= fusion(x', y')`
/// - Non-trivial: there exist `a ≠ b`
pub trait EpistemicCalculus: PartialOrd + Clone {
    fn fusion(x: &Self, y: &Self) -> Self;
    fn unit() -> Self;
}

// Theorem preserved: fusion_unit_right
pub fn fusion_unit_right<V: EpistemicCalculus>(x: &V) -> V {
    // Lean proof: rw [fusion_comm, fusion_unit_left]
    V::fusion(x, &V::unit())
}

// Theorem preserved: fusion_mono_left
// Theorem preserved: fusion_mono_right
// Theorem preserved: fusion_mono'

/// E1: Optimistic — a top element exists.
pub trait Optimistic: EpistemicCalculus {
    fn top() -> Self;
}

/// E4: Closed — internal hom (residuation) exists.
pub trait Closed: EpistemicCalculus {
    fn ihom(y: &Self, z: &Self) -> Self;
}

/// E6: Idempotent fusion.
pub trait IdempotentFusion: EpistemicCalculus {}
// Invariant: fusion(x, x) = x

/// E7: Fallible/revisable.
pub trait Fallible: EpistemicCalculus {
    fn revisable_witness(x: &Self, y: &Self) -> Self;
}

/// E8: Cancellative fusion.
pub trait Cancellative: EpistemicCalculus {}
// Invariant: fusion(x, z) <= fusion(y, z) ⟹ x <= y

#[cfg(test)]
mod tests {
    use super::*;

    // Basic trait bound test — see concrete instances for real tests
    fn assert_has_unit<V: EpistemicCalculus>() {
        let u = V::unit();
        let _ = V::fusion(&u, &u);
    }

    #[test]
    fn trait_compiles() {
        assert_has_unit::<crate::certainty_factors::CF>();
        assert_has_unit::<crate::possibility_theory::PT>();
    }
}