- | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
- match t1,t2 with
- ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
- (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
- when (uri1 = uri2) && (typeno1 = typeno2) &&
- (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
- (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac
- | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
- (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
- when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
- let rec traverse_list i l1 l2 =
- match l1,l2 with
- [],[] -> T.id_tac
- | hd1::tl1,hd2::tl2 ->
- T.then_
- ~start:(injection1_tac ~i ~term)
- ~continuation:(traverse_list (i+1) tl1 tl2)
- | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
- in traverse_list 1 applist1 applist2
- | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
- (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
- | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
- (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
- | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
- (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
- | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
- (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
- when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
- (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac
- | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac
- )
- | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
- )
- | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
- ) status
+ | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
+ begin
+ match t1,t2 with
+ ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
+ (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
+ when (uri1 = uri2) && (typeno1 = typeno2) &&
+ (consno1 = consno2) &&
+ (exp_named_subst1 = exp_named_subst2)
+ ->
+ if first_time then
+ raise
+ (ProofEngineTypes.Fail (lazy "Injection: nothing to do"))
+ else
+ continuation ~liftno
+ | C.Appl
+ ((C.MutConstruct
+ (uri1,typeno1,consno1,exp_named_subst1))::applist1),
+ C.Appl
+ ((C.MutConstruct
+ (uri2,typeno2,consno2,exp_named_subst2))::applist2)
+ when (uri1 = uri2) && (typeno1 = typeno2) &&
+ (consno1 = consno2) &&
+ (exp_named_subst1 = exp_named_subst2)
+ ->
+ let rec traverse_list i l1 l2 =
+ match l1,l2 with
+ [],[] ->
+ if first_time then
+ continuation
+ else
+ (match term with
+ C.Rel n ->
+ (match List.nth context (n-1) with
+ Some (C.Name id,_) ->
+ fun ~liftno ->
+ T.then_
+ ~start:
+ (ProofEngineStructuralRules.clear
+ ~hyps:[id])
+ ~continuation:(continuation ~liftno)
+ | _ -> assert false)
+ | _ -> assert false)
+ | hd1::tl1,hd2::tl2 ->
+ if
+ fst
+ (CicReduction.are_convertible ~metasenv
+ context hd1 hd2 CicUniv.empty_ugraph)
+ then
+ traverse_list (i+1) tl1 tl2
+ else
+ injection1_tac ~i ~term
+ ~continuation:(traverse_list (i+1) tl1 tl2)
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
+ in
+ traverse_list 1 applist1 applist2 ~liftno
+ | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
+ (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
+ | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
+ (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
+ | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
+ (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
+ | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
+ (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
+ when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
+ raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))
+ | _ ->
+ if first_time then
+ raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
+ else
+ continuation ~liftno
+ end
+ | _ ->
+ if first_time then
+ raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
+ else
+ continuation ~liftno
+ end
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
+ ) status