From be4b675b1af2e2b595b8f051e6ab5a7328d6ada2 Mon Sep 17 00:00:00 2001
From: Mroik <mroik@delayed.space>
Date: Tue, 7 May 2024 05:57:02 +0200
Subject: [PATCH] Add absurdum elimination

---
 src/app.rs   |  2 ++
 src/fitch.rs | 26 ++++++++++++++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/src/app.rs b/src/app.rs
index 1c75a21..f331978 100644
--- a/src/app.rs
+++ b/src/app.rs
@@ -98,6 +98,8 @@ enum State {
 enum AbsurdumState {
     IntroduceGetAssumption1,
     IntroduceGetAssumption2(usize),
+    EliminateGetAssumption,
+    EliminateGetProposition(usize),
 }
 
 #[derive(PartialEq)]
diff --git a/src/fitch.rs b/src/fitch.rs
index 12ca52f..91eabe6 100644
--- a/src/fitch.rs
+++ b/src/fitch.rs
@@ -334,6 +334,21 @@ impl Fitch {
         true
     }
 
+    pub fn eliminate_absurdum(&mut self, absurdum: usize, introduce: &Rc<Proposition>) -> bool {
+        match self.statements.get(absurdum) {
+            Some((level, m))
+                if m.unwrap() == &Proposition::new_absurdum() && *level <= self.current_level =>
+            {
+                self.statements.push((
+                    self.current_level,
+                    FitchComponent::Deduction(introduce.clone()),
+                ));
+                true
+            }
+            _ => false,
+        }
+    }
+
     pub fn introduce_not(&mut self, sub_proof: usize) -> bool {
         match self.get_subproof_result(sub_proof) {
             None => return false,
@@ -545,6 +560,17 @@ mod tests {
         );
     }
 
+    #[test]
+    fn eliminate_absurdum() {
+        let mut fitch = Fitch::new();
+        let t0 = Proposition::new_absurdum();
+        let t1 = Proposition::new_term("A");
+        fitch.add_assumption(&t0);
+        let ris = fitch.eliminate_absurdum(0, &t1);
+        assert!(ris);
+        assert_eq!(fitch.statements.last().unwrap().1.unwrap(), &t1);
+    }
+
     #[test]
     fn introduce_not() {
         let mut fitch = Fitch::new();