## Coverage Report

#### Created: 2025-09-08 21:26

next uncovered line (L), next uncovered region (R), next uncovered branch (B)

    /home/noah/src/ruchy/src/proving/tactics.rs

    Line
    Count
    Source
    1
    //! Proof tactics library with ML-powered suggestions
    2
    3
    use anyhow::Result;
    4
    use serde::{Deserialize, Serialize};
    5
    use std::collections::HashMap;
    6
    7
    use super::prover::{ProofGoal, ProofContext, StepResult};
    8
    9
    /// A proof tactic
    10
    pub trait Tactic: Send + Sync {
    11
        /// Get tactic name
    12
        fn name(&self) -> &str;
    13
    14
        /// Get tactic description
    15
        fn description(&self) -> &str;
    16
    17
        /// Apply the tactic to a goal
    18
        fn apply(&self, goal: &ProofGoal, args: &[&str], context: &ProofContext) -> Result<StepResult>;
    19
    20
        /// Check if tactic is applicable
    21
        fn is_applicable(&self, goal: &ProofGoal, context: &ProofContext) -> bool;
    22
    }
    23
    24
    /// Library of available tactics
    25
    pub struct TacticLibrary {
    26
        /// Available tactics
    27
        tactics: HashMap<String, Box<dyn Tactic>>,
    28
    29
        /// ML model for suggestions (placeholder)
    30
        _suggestion_model: SuggestionModel,
    31
    }
    32
    33
    /// ML model for tactic suggestions
    34
    struct SuggestionModel {
    35
        // Placeholder for ML model
    36
    }
    37
    38
    /// Tactic suggestion with confidence
    39
    #[derive(Debug, Clone, Serialize, Deserialize)]
    40
    pub struct TacticSuggestion {
    41
        /// Tactic name
    42
        pub tactic_name: String,
    43
    44
        /// Confidence score (0.0 - 1.0)
    45
        pub confidence: f64,
    46
    47
        /// Reason for suggestion
    48
        pub reason: Option<String>,
    49
    50
        /// Suggested arguments
    51
        pub arguments: Vec<String>,
    52
    }
    53
    54
    impl TacticLibrary {
    55
        /// Create default tactic library
    56
    0
        pub fn default() -> Self {
    57
    0
            let mut tactics = HashMap::new();
    58
    59
            // Add basic tactics
    60
    0
            tactics.insert("intro".to_string(), Box::new(IntroTactic) as Box<dyn Tactic>);
    61
    0
            tactics.insert("split".to_string(), Box::new(SplitTactic) as Box<dyn Tactic>);
    62
    0
            tactics.insert("induction".to_string(), Box::new(InductionTactic) as Box<dyn Tactic>);
    63
    0
            tactics.insert("contradiction".to_string(), Box::new(ContradictionTactic) as Box<dyn Tactic>);
    64
    0
            tactics.insert("reflexivity".to_string(), Box::new(ReflexivityTactic) as Box<dyn Tactic>);
    65
    0
            tactics.insert("simplify".to_string(), Box::new(SimplifyTactic) as Box<dyn Tactic>);
    66
    0
            tactics.insert("unfold".to_string(), Box::new(UnfoldTactic) as Box<dyn Tactic>);
    67
    0
            tactics.insert("rewrite".to_string(), Box::new(RewriteTactic) as Box<dyn Tactic>);
    68
    0
            tactics.insert("apply".to_string(), Box::new(ApplyTactic) as Box<dyn Tactic>);
    69
    0
            tactics.insert("assumption".to_string(), Box::new(AssumptionTactic) as Box<dyn Tactic>);
    70
    71
    0
            Self {
    72
    0
                tactics,
    73
    0
                _suggestion_model: SuggestionModel {},
    74
    0
            }
    75
    0
        }
    76
    77
        /// Get all tactics
    78
    0
        pub fn all_tactics(&self) -> Vec<&dyn Tactic> {
    79
    0
            self.tactics.values().map(std::convert::AsRef::as_ref).collect()
    80
    0
        }
    81
    82
        /// Get a specific tactic
    83
    0
        pub fn get_tactic(&self, name: &str) -> Result<&dyn Tactic> {
    84
    0
            self.tactics.get(name)
    85
    0
                .map(std::convert::AsRef::as_ref)
    86
    0
                .ok_or_else(|| anyhow::anyhow!("Unknown tactic: {}", name))
    87
    0
        }
    88
    89
        /// Suggest tactics for a goal
    90
    0
        pub fn suggest_tactics(&self, goal: &ProofGoal, context: &ProofContext) -> Result<Vec<TacticSuggestion>> {
    91
    0
            let mut suggestions = Vec::new();
    92
    93
            // Check each tactic's applicability
    94
    0
            for (name, tactic) in &self.tactics {
    95
    0
                if tactic.is_applicable(goal, context) {
    96
    0
                    let confidence = self.calculate_confidence(goal, tactic.as_ref());
    97
    0
                    suggestions.push(TacticSuggestion {
    98
    0
                        tactic_name: name.clone(),
    99
    0
                        confidence,
    100
    0
                        reason: Some(format!("Pattern matches {}", tactic.description())),
    101
    0
                        arguments: Vec::new(),
    102
    0
                    });
    103
    0
                }
    104
            }
    105
    106
            // Sort by confidence
    107
    0
            suggestions.sort_by(|a, b| b.confidence.partial_cmp(&a.confidence).unwrap());
    108
    109
    0
            Ok(suggestions)
    110
    0
        }
    111
    112
        /// Calculate confidence for a tactic
    113
    0
        fn calculate_confidence(&self, goal: &ProofGoal, _tactic: &dyn Tactic) -> f64 {
    114
            // Simple heuristic-based confidence
    115
    0
            match &goal.statement {
    116
    0
                s if s.contains("->") => 0.8,  // Implication
    117
    0
                s if s.contains("&&") => 0.7,  // Conjunction
    118
    0
                s if s.contains("||") => 0.6,  // Disjunction
    119
    0
                s if s.contains("==") => 0.9,  // Equality
    120
    0
                _ => 0.5,
    121
            }
    122
    0
        }
    123
    }
    124
    125
    // Basic tactic implementations
    126
    127
    /// Introduction tactic (for implications)
    128
    struct IntroTactic;
    129
    130
    impl Tactic for IntroTactic {
    131
    0
        fn name(&self) -> &'static str { "intro" }
    132
    133
    0
        fn description(&self) -> &'static str { "Introduce hypothesis from implication" }
    134
    135
    0
        fn apply(&self, goal: &ProofGoal, _args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    136
    0
            if goal.statement.contains("->") {
    137
    0
                let parts: Vec<&str> = goal.statement.split("->").collect();
    138
    0
                if parts.len() == 2 {
    139
    0
                    return Ok(StepResult::Simplified(parts[1].trim().to_string()));
    140
    0
                }
    141
    0
            }
    142
    0
            Ok(StepResult::Failed("Cannot apply intro".to_string()))
    143
    0
        }
    144
    145
    0
        fn is_applicable(&self, goal: &ProofGoal, _context: &ProofContext) -> bool {
    146
    0
            goal.statement.contains("->")
    147
    0
        }
    148
    }
    149
    150
    /// Split tactic (for conjunctions)
    151
    struct SplitTactic;
    152
    153
    impl Tactic for SplitTactic {
    154
    0
        fn name(&self) -> &'static str { "split" }
    155
    156
    0
        fn description(&self) -> &'static str { "Split conjunction into subgoals" }
    157
    158
    0
        fn apply(&self, goal: &ProofGoal, _args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    159
    0
            if goal.statement.contains("&&") {
    160
    0
                let parts: Vec<&str> = goal.statement.split("&&").collect();
    161
    0
                let subgoals: Vec<String> = parts.iter().map(|p| p.trim().to_string()).collect();
    162
    0
                return Ok(StepResult::Subgoals(subgoals));
    163
    0
            }
    164
    0
            Ok(StepResult::Failed("Cannot apply split".to_string()))
    165
    0
        }
    166
    167
    0
        fn is_applicable(&self, goal: &ProofGoal, _context: &ProofContext) -> bool {
    168
    0
            goal.statement.contains("&&")
    169
    0
        }
    170
    }
    171
    172
    /// Induction tactic
    173
    struct InductionTactic;
    174
    175
    impl Tactic for InductionTactic {
    176
    0
        fn name(&self) -> &'static str { "induction" }
    177
    178
    0
        fn description(&self) -> &'static str { "Proof by induction" }
    179
    180
    0
        fn apply(&self, goal: &ProofGoal, args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    181
    0
            if args.is_empty() {
    182
    0
                return Ok(StepResult::Failed("Induction requires a variable".to_string()));
    183
    0
            }
    184
    185
    0
            let var = args[0];
    186
    0
            Ok(StepResult::Subgoals(vec![
    187
    0
                format!("Base case: {} when {} = 0", goal.statement, var),
    188
    0
                format!("Inductive step: {} implies {}",
    189
    0
                    goal.statement.replace(var, &var.to_string()),
    190
    0
                    goal.statement.replace(var, &format!("{var}+1"))
    191
    0
                ),
    192
    0
            ]))
    193
    0
        }
    194
    195
    0
        fn is_applicable(&self, goal: &ProofGoal, _context: &ProofContext) -> bool {
    196
    0
            goal.statement.contains("forall") || goal.statement.contains('n')
    197
    0
        }
    198
    }
    199
    200
    /// Contradiction tactic
    201
    struct ContradictionTactic;
    202
    203
    impl Tactic for ContradictionTactic {
    204
    0
        fn name(&self) -> &'static str { "contradiction" }
    205
    206
    0
        fn description(&self) -> &'static str { "Proof by contradiction" }
    207
    208
    0
        fn apply(&self, _goal: &ProofGoal, _args: &[&str], context: &ProofContext) -> Result<StepResult> {
    209
            // Check for contradictory assumptions
    210
    0
            for assumption in &context.assumptions {
    211
    0
                if assumption.contains('!') {
    212
    0
                    let negated = assumption.replace('!', "");
    213
    0
                    if context.assumptions.contains(&negated) {
    214
    0
                        return Ok(StepResult::Solved);
    215
    0
                    }
    216
    0
                }
    217
            }
    218
    0
            Ok(StepResult::Failed("No contradiction found".to_string()))
    219
    0
        }
    220
    221
    0
        fn is_applicable(&self, _goal: &ProofGoal, context: &ProofContext) -> bool {
    222
    0
            context.assumptions.len() >= 2
    223
    0
        }
    224
    }
    225
    226
    /// Reflexivity tactic
    227
    struct ReflexivityTactic;
    228
    229
    impl Tactic for ReflexivityTactic {
    230
    0
        fn name(&self) -> &'static str { "reflexivity" }
    231
    232
    0
        fn description(&self) -> &'static str { "Prove equality by reflexivity" }
    233
    234
    0
        fn apply(&self, goal: &ProofGoal, _args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    235
    0
            if goal.statement.contains("==") {
    236
    0
                let parts: Vec<&str> = goal.statement.split("==").collect();
    237
    0
                if parts.len() == 2 && parts[0].trim() == parts[1].trim() {
    238
    0
                    return Ok(StepResult::Solved);
    239
    0
                }
    240
    0
            }
    241
    0
            Ok(StepResult::Failed("Terms are not equal".to_string()))
    242
    0
        }
    243
    244
    0
        fn is_applicable(&self, goal: &ProofGoal, _context: &ProofContext) -> bool {
    245
    0
            goal.statement.contains("==")
    246
    0
        }
    247
    }
    248
    249
    /// Simplify tactic
    250
    struct SimplifyTactic;
    251
    252
    impl Tactic for SimplifyTactic {
    253
    0
        fn name(&self) -> &'static str { "simplify" }
    254
    255
    0
        fn description(&self) -> &'static str { "Simplify expression" }
    256
    257
    0
        fn apply(&self, goal: &ProofGoal, _args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    258
    0
            let mut simplified = goal.statement.clone();
    259
    260
            // Basic simplifications
    261
    0
            simplified = simplified.replace("true && ", "");
    262
    0
            simplified = simplified.replace(" && true", "");
    263
    0
            simplified = simplified.replace("false || ", "");
    264
    0
            simplified = simplified.replace(" || false", "");
    265
    0
            simplified = simplified.replace("!!!", "!");
    266
    0
            simplified = simplified.replace("!!", "");
    267
    268
    0
            if simplified == goal.statement {
    269
    0
                Ok(StepResult::Failed("No simplification possible".to_string()))
    270
            } else {
    271
    0
                Ok(StepResult::Simplified(simplified))
    272
            }
    273
    0
        }
    274
    275
    0
        fn is_applicable(&self, _goal: &ProofGoal, _context: &ProofContext) -> bool {
    276
    0
            true
    277
    0
        }
    278
    }
    279
    280
    /// Unfold tactic
    281
    struct UnfoldTactic;
    282
    283
    impl Tactic for UnfoldTactic {
    284
    0
        fn name(&self) -> &'static str { "unfold" }
    285
    286
    0
        fn description(&self) -> &'static str { "Unfold definition" }
    287
    288
    0
        fn apply(&self, goal: &ProofGoal, args: &[&str], context: &ProofContext) -> Result<StepResult> {
    289
    0
            if args.is_empty() {
    290
    0
                return Ok(StepResult::Failed("Unfold requires a definition name".to_string()));
    291
    0
            }
    292
    293
    0
            let def_name = args[0];
    294
    0
            if let Some(definition) = context.definitions.get(def_name) {
    295
    0
                let unfolded = goal.statement.replace(def_name, definition);
    296
    0
                Ok(StepResult::Simplified(unfolded))
    297
            } else {
    298
    0
                Ok(StepResult::Failed(format!("Unknown definition: {def_name}")))
    299
            }
    300
    0
        }
    301
    302
    0
        fn is_applicable(&self, _goal: &ProofGoal, context: &ProofContext) -> bool {
    303
    0
            !context.definitions.is_empty()
    304
    0
        }
    305
    }
    306
    307
    /// Rewrite tactic
    308
    struct RewriteTactic;
    309
    310
    impl Tactic for RewriteTactic {
    311
    0
        fn name(&self) -> &'static str { "rewrite" }
    312
    313
    0
        fn description(&self) -> &'static str { "Rewrite using equality" }
    314
    315
    0
        fn apply(&self, goal: &ProofGoal, args: &[&str], context: &ProofContext) -> Result<StepResult> {
    316
    0
            if args.is_empty() {
    317
    0
                return Ok(StepResult::Failed("Rewrite requires an equality".to_string()));
    318
    0
            }
    319
    320
            // Find equality in assumptions
    321
    0
            for assumption in &context.assumptions {
    322
    0
                if assumption.contains("==") {
    323
    0
                    let parts: Vec<&str> = assumption.split("==").collect();
    324
    0
                    if parts.len() == 2 {
    325
    0
                        let lhs = parts[0].trim();
    326
    0
                        let rhs = parts[1].trim();
    327
    0
                        let rewritten = goal.statement.replace(lhs, rhs);
    328
    0
                        if rewritten != goal.statement {
    329
    0
                            return Ok(StepResult::Simplified(rewritten));
    330
    0
                        }
    331
    0
                    }
    332
    0
                }
    333
            }
    334
    335
    0
            Ok(StepResult::Failed("No applicable rewrite found".to_string()))
    336
    0
        }
    337
    338
    0
        fn is_applicable(&self, _goal: &ProofGoal, context: &ProofContext) -> bool {
    339
    0
            context.assumptions.iter().any(|a| a.contains("=="))
    340
    0
        }
    341
    }
    342
    343
    /// Apply tactic
    344
    struct ApplyTactic;
    345
    346
    impl Tactic for ApplyTactic {
    347
    0
        fn name(&self) -> &'static str { "apply" }
    348
    349
    0
        fn description(&self) -> &'static str { "Apply theorem or lemma" }
    350
    351
    0
        fn apply(&self, _goal: &ProofGoal, args: &[&str], _context: &ProofContext) -> Result<StepResult> {
    352
    0
            if args.is_empty() {
    353
    0
                return Ok(StepResult::Failed("Apply requires a theorem name".to_string()));
    354
    0
            }
    355
    356
            // In a real implementation, this would look up theorems
    357
    0
            Ok(StepResult::Failed(format!("Cannot apply theorem: {}", args[0])))
    358
    0
        }
    359
    360
    0
        fn is_applicable(&self, _goal: &ProofGoal, _context: &ProofContext) -> bool {
    361
    0
            true
    362
    0
        }
    363
    }
    364
    365
    /// Assumption tactic
    366
    struct AssumptionTactic;
    367
    368
    impl Tactic for AssumptionTactic {
    369
    0
        fn name(&self) -> &'static str { "assumption" }
    370
    371
    0
        fn description(&self) -> &'static str { "Prove using an assumption" }
    372
    373
    0
        fn apply(&self, goal: &ProofGoal, _args: &[&str], context: &ProofContext) -> Result<StepResult> {
    374
    0
            if context.assumptions.contains(&goal.statement) {
    375
    0
                Ok(StepResult::Solved)
    376
            } else {
    377
    0
                Ok(StepResult::Failed("Goal not in assumptions".to_string()))
    378
            }
    379
    0
        }
    380
    381
    0
        fn is_applicable(&self, goal: &ProofGoal, context: &ProofContext) -> bool {
    382
    0
            context.assumptions.contains(&goal.statement)
    383
    0
        }
    384
    }