fact: Definition gen_match_from_to (T1 T2 : Type) X (offset : nat) : M (forall recursor : T1 -> M T2, forall base : T2 -> M X, T1 -> M X) := i1 <- get_ind_cts T1 O; i2 <- get_ind_cts T2 offset; mmatch (m: i1, i2) with | [?(n1 : nat) (Cs1 : mlist (NDCTele (@iBase Typeₛ T1))) (n2 : nat) (Cs2 : mlist (NDCTele (@iBase Typeₛ T2)))] (m: ((n1, existT _ Typeₛ (existT _ (@iBase Typeₛ T1) Cs1))), ((n2, existT _ Typeₛ (existT _ (@iBase Typeₛ T2) Cs2))) ) => let it1 := @iBase Typeₛ T1 in let it2 := @iBase Typeₛ T2 in (if Nat.eqb (mlength Cs1) (mlength Cs2) then M.ret unit else M.failwith "Number of remaining constructors of T2 does not match that of T1");; let zipped := combine Cs1 Cs2 in \sfnu "recursor" for recursor : T1 -> M T2, \sfnu "base" for base : T2 -> M X, pats <- M.map (fun Csi => let (Cs1_i, Cs2_i) := Csi : (NDCTele it1) *m NDCTele (it2) in let c11 := reduce (RedVmCompute) (projT1 Cs1_i) in let c1 := reduce (RedVmCompute) (projT2 Cs1_i) in let c21 := reduce (RedVmCompute) (projT1 Cs2_i) in let c2 := reduce (RedVmCompute) (projT2 Cs2_i) in t <- gen_match_branch recursor base c11 c21 c1 (fun x => let '(existT _ _ y) := c2 x in base y); M.ret (Dyn t) ) (zipped); \sfnu "t1" for t1 : T1, c <- M.makecase (mkCase T1 t1 (Dyn (fun _ : T1 => M X)) (pats)); dcase c as T, b in oeq <- M.unify (T) (M X) UniCoq; match oeq return (T) -> M ((T1 -> M T2) -> (T2 -> M X) -> T1 -> M X) with | mSome eq => match eq in _ =m= R return T -> M ((T1 -> M T2) -> (T2 -> M X) -> T1 -> R) with | meq_refl => fun f => let ty := T in f <- M.abs_fun (P:=fun _ => ty) t1 f; f <- M.abs_fun base f; f <- M.abs_fun recursor f; M.ret (f) end | mNone => fun _ => M.failwith "Impossible branch." end b end .
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List Sorts DepDestruct MTeleMatch)