/// Lean 4 → Rust transpilation: SupportIsSearch.Refutation
/// Source: SupportIsSearch/Refutation.lean (209 lines)
///
/// Theorem preserved: imp_forward_axiom_refuted
///
/// Computational verification that the standalone implication-forward
/// schema is false on atomic-base kernels.

use crate::syntax::*;
use crate::ipl::IPL;
use crate::encoding::encode;
use crate::kernel::search_supports;

/// Verify the refutation witness:
/// B = {}, phi = (p -> q), psi = q for p = Atom(0), q = Atom(1).
///
/// The conclusion of ImpForwardSchema would require:
///   SearchSupports (encodeBase {}) (encode ((p -> q) -> q))
/// But this is false — ((p -> q) -> q) is not an intuitionistic tautology,
/// and the empty atomic base provides no program clauses to make it searchable.
pub fn verify_refutation(max_fuel: u32) -> bool {
    let p = Atom { id: 0 };
    let q = Atom { id: 1 };

    // Construct (p -> q) -> q
    let p_imp_q = IPL::Imp(Box::new(IPL::Atom(p)), Box::new(IPL::Atom(q)));
    let double_imp = IPL::Imp(Box::new(p_imp_q), Box::new(IPL::Atom(q)));

    let encoded = encode(&double_imp);
    let empty_program: Program = vec![];

    // The conclusion MUST be false for the refutation to hold
    let conclusion = search_supports(&empty_program, &encoded, max_fuel);
    !conclusion
}

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

    #[test]
    fn test_refutation_holds() {
        // The refutation should hold at any reasonable fuel
        assert!(verify_refutation(50));
    }

    #[test]
    fn test_identity_is_searchable() {
        // Sanity: p -> p IS searchable from empty (it's a tautology)
        let p = Atom { id: 0 };
        let identity = IPL::Imp(Box::new(IPL::Atom(p)), Box::new(IPL::Atom(p)));
        let encoded = encode(&identity);
        assert!(search_supports(&vec![], &encoded, 10));
    }

    #[test]
    fn test_peirce_not_searchable() {
        // Peirce's law is not intuitionistically valid
        let p = Atom { id: 0 };
        let q = Atom { id: 1 };
        let peirce = crate::ipl::peirce_formula(p, q);
        let encoded = encode(&peirce);
        assert!(!search_supports(&vec![], &encoded, 20));
    }
}