l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

début de correction d'apply généralisé

Browse Source
This commit is contained in:
Marwan 2024-05-14 11:41:10 +02:00
parent 63c468371f
commit 5ecf82920f
1 changed files with 15 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
proof.ml
View File

@ -198,19 +198,22 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
| Arr (_, t2) -> is_implied goal_ty t2
| _ -> false
in
let rec generate_goals (goal_ty : ty) (t : ty) (cs : context)
(h' : hlam) (h : hlam) (gs : goal list) : proof =
match t with
let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
(goal_h : hlam) (cs : context) (gs : goal list) : proof =
match impl_ty with
Arr (t1, t2) when t2 = goal_ty ->
let new_h = Ref (ref Hole) in
fill h (HApp (h', new_h));
Some (new_h, t1, cs), gs
let sub_h = Ref (ref Hole) in
let _ = fill goal_h (HApp (impl_h, sub_h)) in
Some (sub_h, t1, cs), gs
| Arr (t1, t2) ->
let new_h = Ref (ref Hole) in
let _ = fill h (HApp (h', new_h)) in
let gs = (new_h, t1, cs) :: gs in
generate_goals goal_ty t2 cs h' new_h gs
| _ -> failwith "cannot happen"
(* nouveau sous but *)
let sub_h = Ref (ref Hole) in (* preuve de t1 *)
let new_h = Ref (ref Hole) in (* suite de l'implication *)
let _ = fill impl_h (HApp (HApp (impl_h, sub_h), new_h)) in
let gs = (sub_h, t1, cs) :: gs in
generate_goals goal_ty t2 new_h goal_h cs gs
| _ -> failwith "impossible"
in
let rec get_hyp : context -> (hlam * ty) = function
[] -> raise (TacticFailed "no such hypothesis in context")
@ -222,7 +225,7 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
| Some (h, goal_ty, cs) ->
let h', t' = get_hyp cs in
if is_implied goal_ty t'
then generate_goals goal_ty t' cs h' h gs
then generate_goals goal_ty t' h' h cs gs
else raise (TacticFailed "not an implication")
let tact_intros : proof -> proof =