issue.lp

require open Stdlib.Prop;
require open Stdlib.Impred;
require open Stdlib.Nat;
require open Stdlib.List;
require open Stdlib.Comp;
require open Stdlib.Prod;


// ------------------------------------------------------------------------------
// Reflective contraction for disjunctions
//
// This file implements the logical contraction rule for propositional disjunction
// by proof by reflection.
//
// For example:
// from a proof of  `a ∨ b ∨ b ∨ b ∨ c ∨ c ∨ ⊥`
// we can derive a proof of  `a ∨ b ∨ c ∨ ⊥`
//
// Disjunctions are reified as clauses: lists of Atoms (p i) indexing an
// environment of formulas. The function `den` interprets a clause back into
// a disjunction over this environment.
//
// Clauses are normalized by a mergesort-based procedure using:
//   - split and merge on Atom indices (via compN for ℕ comparison),
//   - remove_iden to delete duplicate atoms from the sorted clause.
// 
// For example, the `a ∨ b ∨ b ∨ b ∨ c ∨ c ∨ ⊥` disjunction is reified
// to the clause `[p 0; p 1; p 1; p 1; p 2; p 2]` (with environment `[a; b; c]`)
// which is contracted to `[p 0; p 1; p 2]` and then interpreted back to
// `a ∨ b ∨ c ∨ ⊥`.
// 
// But this approach sounds to be inefficient because of a `rewrite` step.
// I think this problem is similar to the one of reflective equality checking that we have done in arithmetic.
// 
// ------------------------------------------------------------------------------

// Atoms: syntactic propositional variables indexed by ℕ
inductive Atom : TYPE ≔
| p : ℕ → Atom;

symbol atom : Set;
rule τ atom ↪ Atom;

// Split a list into two lists by alternating elements (for mergesort)
symbol split [a: Set] (l : τ (list a)): τ(list a × list a);
rule split □ ↪ (□ ‚ □)
with split ($x ⸬ □) ↪ (($x ⸬ □) ‚ □)
with split ($x ⸬ $y ⸬ $l) ↪
    let res ≔  (split $l) in
        ($x ⸬ (res ₁)) ‚ ($y ⸬ (res ₂));

// den σ g interprets a list of atoms g as a disjunction of σ's entries
symbol den: 𝕃 o → 𝕃 atom → Prop;
rule den $σ □ ↪ ⊥
with den $σ ((p $i) ⸬ $xs) ↪ (nth ⊥ $σ $i) ∨ (den $σ $xs);

// Index / New: result of searching an element in a list
constant symbol R : TYPE;
constant symbol Index : ℕ → R;
constant symbol New : ℕ → R;

symbol case [a] : R → (ℕ → τ a) → (ℕ → τ a) → τ a;

rule case (Index $i) $f _ ↪ $f $i
with case (New $i) _ $g ↪ $g $i;

sequential symbol index: ℕ → Π [a], τ a → τ(list a) → R;

rule index $k _ □ ↪ New $k
with index $k $x ($x ⸬ _) ↪ Index $k
with index $k $x ($y ⸬ $l) ↪ index ($k +1) $x $l;

// Reify a disjunction φ to a clause (as disjunction) + updated environment σ
// ensuring den σ' g = φ
symbol rfy_disj: 𝕃 o → Prop → τ (list atom × list o);
rule rfy_disj $l ⊥ ↪ (□ ‚ $l)
with rfy_disj $l ($x ∨ $xs) ↪
  let X ≔  case (index 0 $x $l) (λ i, (p i) ‚ $l) (λ i, (p i) ‚ ($l Stdlib.List.++ ($x ⸬ □))) in
  let x ≔ X ₁ in
  let l' ≔ X ₂ in
  let xs ≔ rfy_disj l' $xs in
    ((x ⸬ (xs ₁)) ‚ (xs ₂));

symbol reify_cl ≔ rfy_disj □;

protected symbol compN : ℕ → ℕ → Comp;
rule compN _0 _0 ↪ Eq
with compN _0 (_ +1) ↪ Lt
with compN (_ +1) _0 ↪ Gt
with compN ($x +1) ($y +1) ↪ compN $x $y;

// Merge two sorted lists of atoms (preserving duplicates)
symbol merge  (l1 l2 : τ (list atom)): τ (list atom);
rule merge □ □ ↪ □
with merge □ $l2 ↪ $l2
with merge $l1 □ ↪ $l1
with merge (p $i ⸬ $l1') (p $j ⸬ $l2') ↪
    case_Comp (compN $i $j)
        (p $i ⸬ p $j ⸬ merge $l1' $l2')
        ((p $i) ⸬ merge $l1' (p $j ⸬ $l2'))
        (p $j ⸬ merge (p $i ⸬ $l1') $l2');

// Mergesort: sort a list of atoms using split + merge
symbol mergesort:  τ (list atom) →  τ (list atom);
rule mergesort □ ↪ □
with mergesort ($x ⸬ □) ↪ ($x ⸬ □)
with mergesort ($x ⸬ $y ⸬ $l) ↪
    let s ≔ split ($x ⸬ $y ⸬ $l) in
    let l1 ≔ s ₁ in
    let l2 ≔ s ₂ in
        merge (mergesort l1) (mergesort l2);

// Remove consecutive duplicates from a sorted list
symbol remove_iden: τ (list atom) → τ (list atom);
rule remove_iden □ ↪ □
with remove_iden ((p $i) ⸬ □) ↪ (p $i) ⸬ □
with remove_iden ((p $i) ⸬ (p $j) ⸬ $tl) ↪ case_Comp (compN $i $j)
                                            (remove_iden ((p $j) ⸬ $tl))
                                            ((p $i) ⸬ (remove_iden ((p $j) ⸬ $tl)))
                                            ((p $i) ⸬ (remove_iden ((p $j) ⸬ $tl)));

// Sort and remove duplicates from a clause (as disjunction)
symbol contraction g ≔ remove_iden (mergesort g);

symbol contraction_correct l g : π (den l (contraction g) = den l g);

// ========== TESTS ==========
// Test contraction on a example


// Demo of reflective contraction:
// For this example, the call
//   compute (contraction (r ₁))
// is fast because the reified clause is very short.
// For larger disjunctions (like the commented example_20b below) the same reflective step becomes slow.
// But the compute command is still ~fast but the rewrite step becomes very slow.
opaque symbol example_5b a b : π (a ∨ b ∨ b ∨ b ∨ b ∨ b ∨ ⊥) → π (a ∨ b ∨ ⊥) ≔
begin
  assume a b i;
  set X ≔ (a ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ ⊥))))));
  set Y ≔ (a ∨ b ∨ ⊥);
  have g : π (X = Y) {
    set r ≔ reify_cl X;
    change π (den (r ₂) (r ₁) = Y);
    compute (contraction (r ₁));
    rewrite left contraction_correct;
    reflexivity
  };
  rewrite left g;
  refine i
end;

// Uncomment the following examples to test contraction on larger disjunctions.

// NOTE: ~FAST
// opaque symbol example_10b a b : π (a ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ ⊥) → π (a ∨ b ∨ ⊥) ≔
// begin
//   assume a b i;
//   set X ≔ (a ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ ⊥)))))))))));
//   set Y ≔ (a ∨ b ∨ ⊥);
//   have g : π (X = Y) {
//     set r ≔ reify_cl X;
//     change π (den (r ₂) (r ₁) = Y);
//     rewrite left contraction_correct;
//     reflexivity
//   };
//   rewrite left g;
//   refine i
// end;

// NOTE: ~Start to be slow
// opaque symbol example_15b a b : π (a ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ ⊥) → π (a ∨ b ∨ ⊥) ≔
// begin
//   assume a b i;
//   set X ≔ (a ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ ⊥))))))))))))))));
//   set Y ≔ (a ∨ b ∨ ⊥);
//   have g : π (X = Y) {
//     set r ≔ reify_cl X;
//     change π (den (r ₂) (r ₁) = Y);
//     compute (contraction (r ₁));
//     rewrite left contraction_correct;
//     reflexivity
//   };
//   rewrite left g;
//   refine i
// end;


// NOTE: Whole time 1min24s
// opaque symbol example_20b a b : π (a ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ b ∨ ⊥) → π (a ∨ b ∨ ⊥) ≔
// begin
//   assume a b i;
//   set X ≔ (a ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ (b ∨ ⊥)))))))))))))))))))));
//   set Y ≔ (a ∨ b ∨ ⊥);
//   have g : π (X = Y) {
//     set r ≔ reify_cl X;
//     change π (den (r ₂) (r ₁) = Y);

//     //NOTE: Take 10s
//     //compute (contraction (r ₁));

//     //NOTE: Take ~1min
//     rewrite left contraction_correct;
//     reflexivity
//   };
//   rewrite left g;
//   refine i
// end;