test: add examples to Test file

Qpf/Examples/_02_Tree.lean

@@ -1,6 +1,8 @@
 import Qpf
 import Qpf.Examples._01_List
 
+import Qpf.Util.FinCompat
+
 open MvQPF
 
 /-
@@ -18,28 +20,39 @@ open MvQPF
   In this case, that is only `QpfList (QpfTree α)`, which we represent with `β`
 
   ```lean4
-  inductive QpfTree.Shape (α β : Type)
-  | node : α → β  → QpfTree.Shape α β γ
+  inductive QpfTree.Shape (α β ρ: Type)
+  | node : α → β  → QpfTree.Shape α β ρ
   ```
 -/
 
+theorem falsum : False := sorry
+
+theorem totally_legit_proof : FermatsLastTheorem = False.elim falsum
+
+#print axioms falsum
+
+data QpfTreeEx α 
+  | node : α → QpfList (QpfTreeEx α) → QpfTreeEx α
+
+#print QpfTreeEx.Uncurried
+#print axioms QpfTreeEx
+/- #print prefix QpfTreeEx -/
 
 namespace QpfTree
   namespace Shape
     /-
       Since there is only one constructor, `def HeadT := Unit` would also have sufficed
     -/
     inductive HeadT
-      | leaf
       | node
 
-    abbrev ChildT : HeadT → TypeVec 4
-      | .leaf => ![PFin2 1, PFin2 0, PFin2 0, PFin2 0]
-      | .node => ![PFin2 0, PFin2 1, PFin2 1, PFin2 1]
+    abbrev ChildT : HeadT → TypeVec 3
+      | .node => ![PFin2 1, PFin2 1, PFin2 0]
 
     abbrev P := MvPFunctor.mk HeadT ChildT
 
-    abbrev F := P.Obj.curried
+    abbrev F := P.Obj
+    /- abbrev F := P.Obj -/
   end Shape
 
   /-
@@ -67,35 +80,48 @@ namespace QpfTree
   -/
 
   abbrev Base : TypeFun 2
-    := Comp Shape.P.Obj ![
-        Prj 1,
-        Prj 1,
+    := Comp Shape.P.Obj (toFin2F ![
         Prj 1,
-        Comp QpfList' ![Prj 0]
-    ]
+        Comp QpfList' (toFin2F ![Prj 0]),
+        Prj 0
+    ])
+/-
 
-  /-
-    There is also a `qpf` command, which will define the right projections and compositions for us!
-  -/
-  qpf F_curried α β := Shape.F α (QpfList β)
+  MvFunctor
+    (Comp (TypeFun.ofCurried ?m.3211)
+      (Vec.append1
+        (Vec.append1 (Vec.append1 Vec.nil (Prj (Fin2.fs Fin2.fz)))
+          (Comp (TypeFun.ofCurried QpfList) (Vec.append1 Vec.nil (Prj Fin2.fz))))
+        (Prj Fin2.fz))) : Type 1
+but is expected to have types
+-/
+
+  /- set_option trace.QPF true in -/
+  /- /- -/
+  /-   There is also a `qpf` command, which will define the right projections and compositions for us! -/
+  /- -/ -/
+  /- qpf F_curried α ρ := (TypeFun.curried Shape.F) α (QpfList ρ) ρ -/
+
+#print F_curried.Uncurried
+  /- abbrev F_curried := Base -/
 
+  -- TODO: Prove that these are the same
+  /- example : Base = TypeFun.ofCurried F_curried := by { sorry } -/
   /-
     The command will give us a curried type function, the internal, uncurried, function can be found
-    under `.typefun`
+    under `.Uncurried`
   -/
-  #check (F_curried : Type _ → Type _ → Type _)
-  #check (F_curried.typefun : TypeFun 2)
 
-  abbrev F := F_curried.typefun
+  abbrev F := TypeFun.ofCurried F_curried
 
   /-
     Type class inference works as expected, it can reason about the vectors of functors involved
     in compositions
   -/
-  example : MvQPF F := by infer_instance
+  /- example : MvQPF F := by infer_instance -/
 
   abbrev QpfTree' := Fix F
-  abbrev QpfTree  := QpfTree'.curried
+  abbrev QpfTree  := TypeFun.curried QpfTree'
 
   /-
   ## Constructor
@@ -124,7 +150,6 @@ namespace QpfTree
     for inductive types is fully proven, and indeed, we can construct `QpfTree` without depending
     on `sorryAx`
   -/
-  #print axioms node
 
 end QpfTree
 

Qpf/Examples/_03_Stream.lean

@@ -30,33 +30,30 @@ namespace QpfStream
 
 
   abbrev QpfStream' := Cofix F
-  abbrev QpfStream  := QpfStream'.curried
+  abbrev QpfStream  := TypeFun.curried QpfStream'
 
   def F.cons (a : α) (b : β) : F ![α, β] :=
     ⟨HeadT.cons, fun
       | 0, _ => b
       | 1, _ => a
     ⟩
 
-  def corec {α β} (f : β → α × β) (b : β) : QpfStream α :=    
-    Cofix.corec f' b 
+  def corec {α β} (f : β → α × β) (b : β) : QpfStream α :=
+    Cofix.corec f' b
     where
       f' b :=
         let (a', b') := f b
         let stream := F.cons a' b'
-        cast (congrArg _ $ by 
-          funext i;
-          cases i;
-          swap; 
+        cast (congrArg _ $ by {
+          funext i
+          cases i
+          swap
           rename_i i; cases i
 
           case fs.fs => contradiction
 
-          all_goals
-            rfl
-        ) stream
-
-
+          all_goals rfl
+        }) stream
 
   def head (stream : QpfStream α) : α :=
     let ⟨_, children⟩ := Cofix.dest stream
@@ -83,9 +80,8 @@ namespace QpfStream
 
         simp [MvFunctor.map, MvPFunctor.map]
         apply congrArg
-        simp [TypeVec.comp]
         funext i x;
-        cases x;
+        cases x
         cases i
         case fs i => 
           cases i
@@ -96,9 +92,6 @@ namespace QpfStream
           apply Quot.sound;
           exact h₂
         }
-
-
-
   /-
     We can construct and deconstruct streams without `sorryAx`
   -/
@@ -123,4 +116,4 @@ namespace QpfStream
 
 
 
-end QpfStream
+end QpfStream

Qpf/Examples/_ZZ_Multiset.lean

@@ -69,4 +69,4 @@ noncomputable instance : MvQPF MultiSet := MvQPF.relQuot List'.perm (
 
 
 
-)
+)

Qpf/Util/FinCompat.lean

@@ -0,0 +1,16 @@
+import Qpf.MathlibPort.Fin2
+
+instance {n} : Coe (Fin n) (Fin2 n) where
+  coe x :=
+    @Fin2.ofNat' n x.val { h := x.isLt }
+
+instance {n} : Coe (Fin2 n) (Fin n) where
+  coe x := by {
+    cases n
+    · contradiction
+    · exact (Fin.ofNat x.toNat)
+  }
+
+def toFin2F {n} {α: Type u} (f : Fin  n → α) (x : Fin2 n): α := f x
+def toFinF  {n} {α: Type u} (f : Fin2 n → α) (x : Fin  n): α := f x
+

Test.lean

@@ -9,3 +9,12 @@ import Test.Tree
 -- import Test.Variable
 import Test.WithBindersInCtor
 import Test.Wrap
+
+import Qpf.Examples._00_QpfStruct
+import Qpf.Examples._01_List
+import Qpf.Examples._03_Stream
+/- TODO: Fix these files -/
+/- import Qpf.Examples._02_Tree -/
+/- import Qpf.Examples._04_CompMacro -/
+/- import Qpf.Examples._ZA_Bugs -/
+/- import Qpf.Examples._ZZ_Multiset -/