restart

carcara/lambdapi/Alethe.lp

@@ -138,14 +138,14 @@ begin
       apply ∧ᶜᵢ
         { apply ⇒ᶜᵢ; assume H; apply ∨ᶜᵢ₂; apply H }
         {
-          apply ⇒ᶜᵢ; assume H;
+          apply ⇒ᶜᵢ; assume H; 
           apply ∨ᶜₑ H { assume H⊥; apply ⊥ᶜₑ; apply H⊥ } { assume H1;  apply H1}
         }
     }
     {
       assume x l Hir;
       apply ∧ᶜᵢ
-      { apply ⇒ᶜᵢ; assume H; apply ∨ᶜₑ H
+      { apply ⇒ᶜᵢ; assume H;   apply ∨ᶜₑ H
         {
           assume Hx;
           apply ∨ᶜᵢ₁;
@@ -211,9 +211,9 @@ constant symbol nnpp_eq p : πᶜ ((¬ ¬ p) = p);
 
 // Axiom propositional_extensionality: forall (P Q : Prop), (P <-> Q) -> P = Q.
 // τ o ↪ Prop
-constant symbol prop_ext [p: τ o] [q: τ o]: πᶜ (p ⇔ᶜ q) → πᶜ (p = q);
+constant symbol prop_ext [p: Prop] [q: Prop]: πᶜ (p ⇔ᶜ q) → πᶜ (p = q);
 
-opaque symbol ⟺_ext [p: τ o] [q: τ o]:  πᶜ (p = q) → πᶜ (p ⇔ᶜ q) ≔
+opaque symbol ⟺_ext [p: Prop] [q: Prop]:  πᶜ (p = q) → πᶜ (p ⇔ᶜ q) ≔
 begin
   assume p q Heq;  rewrite Heq; apply ⇔ᶜ_refl
 end;
@@ -471,7 +471,7 @@ end;
 symbol ϵ  [a]: (τ a → Prop) → τ a; notation ϵ quantifier;
 
 constant symbol ϵᵢ [a] x (p: τ a → Prop) : πᶜ (p x) → πᶜ (p (ϵ p));
-constant symbol ϵ_det [p q]: Π x, πᶜ ((p x) ⇔ᶜ (q x)) → πᶜ (ϵ p = ϵ q);
+constant symbol ϵ_det [a p q]: Π (x: τ a), πᶜ ((p x) ⇔ᶜ (q x)) → πᶜ (ϵ p = ϵ q);
 
 opaque symbol ϵ_to_∃ [a] p: πᶜ ((`∃ᶜ (x : τ a),  p x) = p (`ϵ (x : τ a), p x)) ≔
 begin
@@ -561,9 +561,9 @@ begin
   { apply ⇒ᶜᵢ; assume Hx; apply ∨ᶜᵢ₁; refine Hx }
 end;
 
-opaque symbol ϵ_equiv_∃ᶜ' [p] : πᶜ ((`∃ᶜ x, p x) = (p (`ϵ x, p x))) ≔
+opaque symbol ϵ_equiv_∃ᶜ' [a p] : πᶜ ((`∃ᶜ (x: τ a), p x) = (p (`ϵ x, p x))) ≔
 begin
-  assume p;
+  assume a p;
   apply prop_ext;
   apply ∧ᶜᵢ
   {
@@ -582,9 +582,9 @@ begin
   } 
 end;
 
-opaque symbol ϵ_equiv_∃ᶜ [p] : πᶜ ((`∃ᶜ x, p x) ⇔ᶜ (p (`ϵ x, p x))) ≔
+opaque symbol ϵ_equiv_∃ᶜ [a p] : πᶜ ((`∃ᶜ x: τ a, p x) ⇔ᶜ (p (`ϵ x, p x))) ≔
 begin
-  assume p;
+  assume a p;
   apply ∧ᶜᵢ
   {
     apply ⇒ᶜᵢ;
@@ -679,7 +679,6 @@ begin
     reflexivity
 end;
 
-
 opaque symbol ite_pos1 [c t e] : π̇ ((¬ (ite c t e)) ⟇ c ⟇ e ⟇ ▩) ≔
 begin
   assume c t e;
@@ -1125,6 +1124,13 @@ begin
   apply classic
 end;
 
+opaque symbol not_symm [a] [x y: τ a] : πᶜ (¬ (x = y)) → πᶜ (¬ (y = x)) ≔
+begin
+  simplify;
+  assume a x y H;
+  admit
+end;
+
 opaque symbol subproof1 [φ₁ ψ] : πᶜ φ₁ → πᶜ ψ → π̇ ((¬ φ₁) ⟇ ψ ⟇ ▩) ≔
 begin
   assume φ₁ ψ Hφ₁ Hψ;
@@ -1163,27 +1169,52 @@ begin
   apply Hψ;
 end;
 
-opaque symbol forall_inst1 p x : πᶜ (¬ (`∀ᶜ x', p x') ∨ᶜ (p x)) ≔
+opaque symbol subproof5 [φ₁ φ₂ φ₃ φ₄ φ₅ ψ] : πᶜ φ₁ → πᶜ φ₂ → πᶜ φ₃ → πᶜ φ₄ → πᶜ φ₅ → πᶜ ψ → π̇ ((¬ φ₁) ⟇ (¬ φ₂) ⟇ (¬ φ₃) ⟇ (¬ φ₄) ⟇ (¬ φ₅) ⟇ ψ ⟇ ▩) ≔
+begin
+  assume φ₁ φ₂ φ₃ φ₄ φ₅ ψ Hφ₁ Hφ₂ Hφ₃ Hφ₄ Hφ₅ Hψ;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₁;
+  apply Hψ;
+end;
+
+opaque symbol subproof6 [φ₁ φ₂ φ₃ φ₄ φ₅ φ₆ ψ] : πᶜ φ₁ → πᶜ φ₂ → πᶜ φ₃ → πᶜ φ₄ → πᶜ φ₅ → πᶜ φ₆ → πᶜ ψ → π̇ ((¬ φ₁) ⟇ (¬ φ₂) ⟇ (¬ φ₃) ⟇ (¬ φ₄) ⟇ (¬ φ₅) ⟇ (¬ φ₆) ⟇ ψ ⟇ ▩) ≔
 begin
- assume p x;
+  assume φ₁ φ₂ φ₃ φ₄ φ₅ φ₆ ψ Hφ₁ Hφ₂ Hφ₃ Hφ₄ Hφ₅ Hφ₆ Hψ;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₂;
+  apply ∨ᶜᵢ₁;
+  apply Hψ;
+end;
+
+opaque symbol forall_inst1 [a] p (x: τ a) : πᶜ (¬ (`∀ᶜ x', p x') ∨ᶜ (p x)) ≔
+begin
+ assume a p x;
  rewrite imp_eq_or;
  apply ⇒ᶜᵢ;
  assume H;
  apply ∀ᶜₑ x H
 end;
 
-opaque symbol forall_inst2 p x y: πᶜ (¬ (`∀ᶜ a, `∀ᶜ b, p a b) ∨ᶜ (p x y)) ≔
+opaque symbol forall_inst2 [a] p (x y: τ a) : πᶜ (¬ (`∀ᶜ a, `∀ᶜ b, p a b) ∨ᶜ (p x y)) ≔
 begin
-  assume p x y;
+  assume a p x y;
   rewrite imp_eq_or;
   apply ⇒ᶜᵢ;
   assume H;
   apply ∀ᶜₑ y (∀ᶜₑ x H)
  end;
 
-opaque symbol forall_inst3 [p] x y z: πᶜ ((¬ (`∀ᶜ a, `∀ᶜ b, `∀ᶜ c, p a b c)) ∨ᶜ ((p x y z) ∨ᶜ ⊥)) ≔
+opaque symbol forall_inst3 [a] [p] (x y z: τ a) : πᶜ ((¬ (`∀ᶜ a, `∀ᶜ b, `∀ᶜ c, p a b c)) ∨ᶜ ((p x y z) ∨ᶜ ⊥)) ≔
 begin
-  assume p x y z;
+  assume a p x y z;
   apply imply_to_or;
   apply ⇒ᶜᵢ;
   assume H;
@@ -1344,7 +1375,7 @@ opaque symbol resolutionₗ x a b: π̇ (x ⟇ a) → π̇ ((¬ x) ⟇ b) → π
       have tmp:  πᶜ ((⟇_to_∨ᶜ_rw a ∨ᶜ ⟇_to_∨ᶜ_rw b)  ⇒ᶜ ⟇_to_∨ᶜ_rw (a ++ b)) {
         apply ∧ᶜₑ₂ (++_to_∨ᶜ a b);
       };
-      apply ⇒ᶜₑ tmp;
+      apply ⇒ᶜₑ tmp; 
       apply ∨ᶜₑ Hx { assume Hpi_x;  apply ∨ᶜₑ Hnx { assume Hpi_nx;  apply ¬ᶜₑ Hpi_nx Hpi_x }  {  assume Hbot; apply ⊥ᶜₑ;  apply Hbot  } } { assume Hbot; apply ⊥ᶜₑ;  apply Hbot  };
     } {
       assume Hb;
@@ -1419,9 +1450,9 @@ opaque symbol resolutionᵣ x a b: π̇ ((¬ x) ⟇ a) → π̇ (x ⟇ b) → π
   };
 end;
 
-opaque symbol bind_∃ [p q]: (Π x, πᶜ (p x = q x))  → πᶜ ((`∃ᶜ x, p x) = (`∃ᶜ x, q x)) ≔
+opaque symbol bind_∃ [a p q]: (Π x, πᶜ (p x = q x))  → πᶜ ((`∃ᶜ (x: τ a), p x) = (`∃ᶜ (x: τ a), q x)) ≔
 begin
-  assume p q H;
+  assume a p q H;
   apply prop_ext;
   apply ∧ᶜᵢ 
   {
@@ -1535,10 +1566,10 @@ symbol distinct a n : Vec a n → Prop;
 
 //type (cons 2 a (cons 1 b (cons 0 c □)));
 
-// boolean case
+// // boolean case
 rule distinct o _ □ ↪ ⊤
 with distinct o 2 (cons 1 $x (cons 0 $y □)) ↪ ($x ≠ $y)
-with distinct o (_ +1 +1 +1) _ ↪ ⊥;
+with distinct o ((($x +1) +1) +1) _ ↪ ⊥;
 
 compute distinct o 2 ((cons 1 a (cons 0 b □)));
 compute distinct o 3 (cons 2 a (cons _ b (cons _ c □)));
@@ -1574,3 +1605,45 @@ opaque symbol feq3ᶜ [a b c d] (f:τ a → τ b →  τ c → τ d):
 begin
   assume a b c d f x x' xx' y y' yy' z z' zz'; rewrite xx'; rewrite yy'; rewrite zz'; reflexivity
 end;
+
+
+opaque symbol feq4ᶜ [a b c d e] (f:τ a → τ b →  τ c → τ d → τ e):
+  Π [x1 x1':τ a], πᶜ(x1 = x1') →
+  Π [x2 x2':τ b], πᶜ(x2 = x2') →
+  Π [x3 x3':τ c], πᶜ(x3 = x3') →
+  Π [x4 x4':τ d], πᶜ(x4 = x4') →
+  πᶜ(f x1 x2 x3 x4 = f x1' x2' x3' x4') ≔
+begin
+  assume a b c d e f;
+  assume x1 x1' H1;
+  assume x2 x2' H2;
+  assume x3 x3' H3;
+  assume x4 x4' H4;
+  rewrite H1;
+  rewrite H2;
+  rewrite H3;
+  rewrite H4;
+  reflexivity
+end;
+
+opaque symbol feq5ᶜ [a b c d e g] (f:τ a → τ b →  τ c  → τ d → τ e → τ g ):
+  Π [x1 x1':τ a], πᶜ(x1 = x1') →
+  Π [x2 x2':τ b], πᶜ(x2 = x2') →
+  Π [x3 x3':τ c], πᶜ(x3 = x3') →
+  Π [x4 x4':τ d], πᶜ(x4 = x4') →
+  Π [x5 x5':τ e], πᶜ(x5 = x5') →
+  πᶜ(f x1 x2 x3 x4 x5 = f x1' x2' x3' x4' x5') ≔
+begin
+  assume a b c d e g f;
+  assume x1 x1' H1;
+  assume x2 x2' H2;
+  assume x3 x3' H3;
+  assume x4 x4' H4;
+  assume x5 x5' H5;
+  rewrite H1;
+  rewrite H2;
+  rewrite H3;
+  rewrite H4;
+  rewrite H5;
+  reflexivity
+end;

carcara/lambdapi/Classic.lp

@@ -59,30 +59,26 @@ end;
 
 symbol ∀ᶜ [a] p ≔ `∀ x : τ a, ¬ ¬ (p x); notation ∀ᶜ quantifier;
 
-
-opaque symbol ∀ᶜᵢ [a] p: (Π (x: τ a), πᶜ (p x)) → πᶜ (∀ᶜ p) ≔
+opaque symbol ∀ᶜᵢ [a] p : (Π (x: τ a), πᶜ (p x)) → πᶜ (∀ᶜ p) ≔
 begin
-
   assume a p Hnnpx Hnnnpx;
-  simplify;
-  admit
-  // apply Hnnnpx;
-  // simplify;
-  // apply Hnnnpx;
-  // assume Hnp;
-  // apply Hnnp;
-  // apply Hnp
+  apply Hnnnpx;
+  assume x Hnnp;
+  apply Hnnpx x;
+  assume Hnp;
+  apply Hnnp;
+  apply Hnp
 end;
 
 opaque symbol ∀ᶜₑ [a p] (x: τ a) : πᶜ (∀ᶜ p) → πᶜ (p x) ≔
 begin
-  assume p x Hnnforallnnp Hnnpx;
-  admit
-  // apply Hnnforallnnp;
-  // assume Hforallnnp;
-  // refine Hforallnnp x Hnnpx
+  assume a p x Hnnforallnnp Hnnpx;
+  apply Hnnforallnnp;
+  assume Hforallnnp;
+  refine Hforallnnp x Hnnpx
 end;
 
+
 symbol ∃ᶜ [a] p ≔ `∃ x : τ a, ¬ ¬ (p x); notation ∃ᶜ quantifier;
 
 opaque symbol ∃ᶜᵢ [a] p (x: τ a) : πᶜ (p x) → πᶜ (∃ᶜ p) ≔
@@ -154,7 +150,18 @@ begin
   refine Hnnnp Hnnp 
 end;
 
-constant symbol classic [p] : πᶜ (p ∨ᶜ ¬ p);
+opaque symbol classic [p] : πᶜ (p ∨ᶜ ¬ p) ≔
+begin
+  assume p H;
+  apply H;
+  apply ∨ᵢ₁;
+  assume Hnp;
+  apply H;
+  apply ∨ᵢ₂;
+  assume Hnnp;
+  apply Hnnp;
+  refine Hnp
+end;
 
 opaque symbol nnpp [p] : πᶜ (¬ ¬ p) → πᶜ p ≔
 begin

carcara/lambdapi/Rare.lp

@@ -9,7 +9,7 @@ require open lambdapi.Simplify;
 
 
 // (define-rule eq-refl ((t ?)) (= t t) true)
-opaque symbol eq-refl t : πᶜ ((t = t) = ⊤) ≔ equiv_simplify₂ t;
+opaque symbol eq-refl [a] (t: τ a) : πᶜ ((t = t) = ⊤) ≔ equiv_simplify₂ t;
 
 // (define-rule eq-symm ((t ?) (s ?)) (= t s) (= s t))
 opaque symbol eq-symm [a] (t s: τ a) : πᶜ ((t = s) = (s = t)) ≔
@@ -45,9 +45,10 @@ begin
   { apply ⇒ᶜᵢ; assume Hor; apply or_to_imply Hor }
 end;
 
-// (define-rule distinct-binary-elim ((t ?) (s ?)) (distinct t s) (not (= t s)))
-opaque symbol distinct-binary-elim (t s: τ o) : πᶜ (distinct o 2 (cons 1 t (cons 0 s □)) = ( t ≠ s)) ≔
-begin assume t s; reflexivity end;
+//FIXME: (define-rule distinct-binary-elim ((t ?) (s ?)) (distinct t s) (not (= t s)))
+opaque symbol distinct-binary-elim [a] (t s: τ a) : πᶜ (distinct a 2 (cons 1 t (cons 0 s □)) = ( t ≠ s)) ≔
+begin admit end;
+//begin assume a t s; reflexivity end;
 
 
 // (define-rule bool-impl-true2 ((t Bool)) (=> true t) t)

carcara/lambdapi/Simplify.lp

@@ -60,9 +60,9 @@ begin
     }
 end;
 
-symbol equiv_simplify₂ p : πᶜ ((p = p) = ⊤) ≔
+symbol equiv_simplify₂ [a] (p: τ a) : πᶜ ((p = p) = ⊤) ≔
 begin
-    assume p;
+    assume a p;
     apply prop_ext;
     apply ∧ᶜᵢ
     { apply ⇒ᶜᵢ; assume H; remove H; apply trivial }